Lemma Gauss: ∀ n,
    2 * (nsum n (fun i => i)) = n * (n + 1).
\ccForall{n : \ccNat{}}{2 \times \ccNsum{i}{n}{i} =
                        n \times (n + 1)}
  induction n; cbn [nsum].
2 \times 0 = 0 \times (0 + 1)
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} =
n \times (n + 1)
2 \times (\ccSucc{ n} + \ccNsum{i}{n}{i}) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
  - (* n ← 0 *)
2 \times 0 = 0 \times (0 + 1)
    reflexivity.
  - (* n ← S _ *)
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} =
n \times (n + 1)
2 \times (\ccSucc{ n} + \ccNsum{i}{n}{i}) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    rewrite Mult.mult_plus_distr_l.
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} =
n \times (n + 1)
2 \times \ccSucc{ n} + 2 \times \ccNsum{i}{n}{i} =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    rewrite IHn.
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} =
n \times (n + 1)
2 \times \ccSucc{ n} + n \times (n + 1) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    ring.
Qed.