sum.v

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.

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