proposition: Lemma sum_sum3 n : \sum_(0 <= i < n) (6 * i ^ 2 + 6 * i + 2) = 6 * (\sum_(0 <= i < n) i ^ 2) + 3 * n * n.-1 + n.*2.
proof: Proof. rewrite big_split big_split /=. rewrite -!sum_mull sum_gauss_const. by rewrite -mulnA -sum_gauss // -mul2n mulnA muln2. Qed.
imports: mathcomp(all_ssreflect)