Skip to content

Instantly share code, notes, and snippets.

@keigoi keigoi/sum.v
Last active Feb 25, 2018

Embed
What would you like to do?
Require Import Nat.
Require Import Omega. (* fixme *)
Fixpoint sum (n:nat) : nat :=
match n with
| O => O
| S n => S n + sum n
end.
Lemma sum_double : forall (n:nat), sum n * 2 = n * (n + 1).
Proof.
induction n.
trivial.
unfold sum; fold sum.
rewrite Nat.mul_add_distr_r.
rewrite IHn.
Require Import ArithRing.
ring.
Qed.
@keigoi

This comment has been minimized.

Copy link
Owner Author

keigoi commented Feb 25, 2018

ゴミが残ってるのはご愛嬌

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.