proposition: Lemma sum_gauss_alt2 n : (\sum_(0 <= i < n) i).*2 = n * n.-1.
proof: Proof. rewrite -addnn [X in X + _ = _]big_nat_rev -big_split /=. rewrite -[X in _ = X * _]subn0 -sum_nat_const_nat. apply: eq_big_nat => i. by case: n => // n /andP[iP iLn]; rewrite [_ + _]subnK. Qed.
imports: mathcomp(all_ssreflect)