Lemma Gauss: ∀ n,
    2 * (nsum n (fun x => x)) =
    n * (n + 1).
∀ n : nat, 2 * nsum n (λ x : nat, x) = n * (n + 1)
  induction n; cbn [nsum].
2 * 0 = 0 * (0 + 1)
n:nat
IHn:2 * nsum n (λ x : nat, x) = n * (n + 1)
2 * (S n + nsum n (λ x : nat, x)) = S n * (S n + 1)
  - (* n ← 0 *)
2 * 0 = 0 * (0 + 1)
    reflexivity.
  - (* n ← S _ *)
n:nat
IHn:2 * nsum n (λ x : nat, x) = n * (n + 1)
2 * (S n + nsum n (λ x : nat, x)) = S n * (S n + 1)
    rewrite Mult.mult_plus_distr_l.
2 * S n + 2 * nsum n (λ x : nat, x) = S n * (S n + 1)
    rewrite IHn.
2 * S n + n * (n + 1) = S n * (S n + 1)
    ring.
Qed.