proposition: Lemma F13 n: (\sum_(i<n) (i.*2.+1)^2) * 3 = n * (n ^2 * 4 - 1).
proof: Proof. rewrite F13'; case: n => //n. rewrite bin1 mulnDl mulnAC - mulnA - mul_bin_diag/= (mulnC n.+2). rewrite - (mulnA 4 2) (mulnA 2) - mul_bin_diag /= bin1 -mulnA (mulnC 4) - mulnA. rewrite - mulnDr; congr (_ * _); rewrite -addn1 mulnDr mulnDl muln1. by rewrite - mulnn mulSnr mulnDl (mulSnr n 4) (addnA _ 3 1) !addnA addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)