sum.v

(* for 8.6 *)
(* based on https://gist.github.com/keigoi/c3817d2aad09e9179465d4261cf5ef9b *)
(* "using"縛り *)

Require Import PeanoNat.

Fixpoint sum (n:nat) : nat :=
  match n with
  | O => O
  | S n => S n + sum n
  end.

Lemma sum_double : forall (n:nat), n * (n + 1) = sum n * 2.
Proof.
proof.
  let n:nat.
  per induction on n.
  suppose it is O.
    thus thesis.
  suppose it is (S m) and IHm:thesis for m.
    have (S m * (S m + 1) = S m * S m + S m * 1) by Nat.mul_add_distr_l. (* ここからring *)
                         ~=(S m + m * S m + 1 * S m) by Nat.mul_comm.
                         ~=(S m + m * S m + S m) by Nat.mul_1_l.
                         ~=(S m + S m + m * S m) by Nat.add_comm, Nat.add_assoc.
                         ~=(S m * 2 + m * S m) by Nat.mul_1_r, Nat.mul_succ_r.
                         ~=(S m * 2 + m * (1 + m)).
                         ~=(S m * 2 + m * (m + 1)) by Nat.add_comm. (* ここまでring *)
                         ~=(S m * 2 + (sum m * 2)) by IHm.
                         ~=((S m + sum m) * 2) by Nat.mul_add_distr_r.
    thus                 ~=(sum (S m) * 2).
  end induction.
end proof.
Qed.