Lemma Gauss:
  ∀ n, 2 * (sum n) = n * (n + 1).
∀ n : nat, 2 * sum n = n * (n + 1)
Proof.
∀ n : nat, 2 * sum n = n * (n + 1)
  induction n.
2 * sum 0 = 0 * (0 + 1)
n:nat
IHn:2 * sum n = n * (n + 1)
2 * sum (S n) = S n * (S n + 1)
  - (* n ← 0 *)
2 * sum 0 = 0 * (0 + 1)
    reflexivity.
  - (* n ← S _ *)
n:nat
IHn:2 * sum n = n * (n + 1)
2 * sum (S n) = S n * (S n + 1)
    cbn [sum].
n:nat
IHn:2 * sum n = n * (n + 1)
2 * (S n + sum n) = S n * (S n + 1)
    rewrite Mult.mult_plus_distr_l.
n:nat
IHn:2 * sum n = n * (n + 1)
2 * S n + 2 * sum n = S n * (S n + 1)
    rewrite IHn.
n:nat
IHn:2 * sum n = n * (n + 1)
2 * S n + n * (n + 1) = S n * (S n + 1)
    change (S n) with (1 + n).
n:nat
IHn:2 * sum n = n * (n + 1)
2 * (1 + n) + n * (n + 1) = (1 + n) * (1 + n + 1)
    rewrite !Mult.mult_plus_distr_l.
n:nat
IHn:2 * sum n = n * (n + 1)
2 * 1 + 2 * n + (n * n + n * 1) =
(1 + n) * 1 + (1 + n) * n + (1 + n) * 1
    rewrite !Mult.mult_plus_distr_r.
n:nat
IHn:2 * sum n = n * (n + 1)
2 * 1 + 2 * n + (n * n + n * 1) =
1 * 1 + n * 1 + (1 * n + n * n) + (1 * 1 + n * 1)
    cbn [Nat.mul];
      rewrite !Nat.mul_1_r, !Nat.add_0_r.
n:nat
IHn:2 * sum n = n * (n + 1)
1 + 1 + (n + n) + (n * n + n) =
1 + n + (n + n * n) + (1 + n)
    rewrite !Nat.add_assoc.
n:nat
IHn:2 * sum n = n * (n + 1)
1 + 1 + n + n + n * n + n =
1 + n + n + n * n + 1 + n
    change (1 + 1) with 2.
n:nat
IHn:2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 1 + n + n + n * n + 1 + n
    rewrite !(Nat.add_comm _ 1).
n:nat
IHn:2 * sum n = n * (n + 1)
2 + n + n + n * n + n =
1 + (1 + n + n + n * n) + n
    rewrite !Nat.add_assoc.
n:nat
IHn:2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 1 + 1 + n + n + n * n + n
    change (1 + 1) with 2.
n:nat
IHn:2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 2 + n + n + n * n + n
    reflexivity.
Qed.