Skip to content

Instantly share code, notes, and snippets.

@srbmiy

srbmiy/ssrnat002.v

Created December 20, 2014 12:02
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save srbmiy/9c82a2ca96660cc64a87 to your computer and use it in GitHub Desktop.
Save srbmiy/9c82a2ca96660cc64a87 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ssrnat002.v
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