proposition: Lemma sum_gauss n : (\sum_(0 <= i < n) i).*2 = n * n.-1.
proof: Proof. elim: n => [|n IH]; first by rewrite big_geq. rewrite big_nat_recr //= doubleD {}IH. case: n => [|n /=]; first by rewrite muln0. by rewrite -muln2 -mulnDr addn2 mulnC. Qed.
imports: mathcomp(all_ssreflect)