Skip to content

Instantly share code, notes, and snippets.

@srbmiy srbmiy/ssrnat002.v
Created Dec 20, 2014

Embed
What would you like to do?
Require Import ssreflect ssrbool ssrnat.
(* Software Foundation 練習問題: ★★, recommended (basic_induction) *)
Lemma ゼロを掛けるとゼロになる : forall (n:nat), n*0 = 0.
Proof.
move=> n.
induction n as [| m].
trivial. (* 0*0 == 0 *)
rewrite mulSnr. (* m.+1 * 0 ~~~> m * 0 + 0 *)
rewrite -> IHm. (* apply IHm : m * 0 == 0 *)
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.