Skip to content

Instantly share code, notes, and snippets.

@haruyama

haruyama/gist:77e09c70e09d960d9c84234d7c7a3d4b

Last active May 10, 2018 23:35
Show Gist options
  • Save haruyama/77e09c70e09d960d9c84234d7c7a3d4b to your computer and use it in GitHub Desktop.
Save haruyama/77e09c70e09d960d9c84234d7c7a3d4b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
From mathcomp
Require Import ssreflect ssrnat.
Section naturalNumber.
Lemma add0nEqn (n : nat) : 0 + n = n.
Proof. by []. Qed.
Lemma addn3Eq2n1 (n : nat) : n + 3 = 2 + n + 1.
Proof.
rewrite addn1.
rewrite add2n.
rewrite addnC.
by [].
Qed.
Fixpoint sum n := if n is m.+1 then sum m + n else 0.
Lemma sumGauss (n : nat) : sum n * 2 = (n + 1) * n.
Proof.
elim: n => [// | n IHn].
rewrite mulnC.
rewrite (_ : sum (n.+1) = n.+1 + (sum n)); last first.
rewrite /=.
by rewrite addnC.
rewrite mulnDr.
rewrite mulnC in IHn.
rewrite IHn.
rewrite 2!addn1.
rewrite [_ * n]mulnC.
rewrite -mulnDl.
by [].
Qed.
End naturalNumber.
@haruyama
Copy link
Author

https://twitter.com/haruyama/status/994523101374238720 以降のやりとりのために配置した

@haruyama
Copy link
Author

間違いを修正した

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment