proposition: Lemma sum_square_alt n : 6 * (\sum_(0 <= i < n) i ^ 2) = n * n.-1 * n.-1.*2.+1.
proof: Proof. apply: (@addIn (3 * n * n.-1 + n.*2)). rewrite addnA -[6]/(2 * 3) -!mulnA mul2n (big_morph _ (mulnDr _) (muln0 _)). rewrite -{1}sum_gauss -doubleMr (big_morph _ (mulnDr _) (muln0 _)). rewrite -{3}[n]muln1 -{3}[n]subn0 -sum_nat_const_nat. rewrite -!doubleD -!big_split /=. rewrite (eq_big_nat _ _ (_ : forall i, _ -> _ = i.+1 ^ 3 - i ^3)) => [|i H]; last first. rewrite -[LHS](addKn (i ^ 3)); congr (_ - _). by sring. apply: etrans (_ : (n^3).*2 = _). congr (_.*2). elim: n => [|n IH]; first by rewrite big_geq. by rewrite big_nat_recr //= IH addnC subnK // leq_exp2r. by case: n => //= n1; sring. Qed.
imports: mathcomp(all_ssreflect)