proposition: Lemma F13direct n: (\sum_(i<n) ((i*2).+1)^2) * 3 = n * (n ^2 * 4 - 1).
proof: Proof. elim: n; first by rewrite big_ord0. move => n Hrec;rewrite big_ord_recr /= mulnDl Hrec {Hrec}. have aux: forall m, (m.+1) ^2 *4 - 1 = m^2 *4 + m * 8 + 3. move => m; rewrite -(addn1 m) sqrnD muln1 exp1n mulnDl. rewrite mulnDl mul1n - mulnAC addnAC - (mulnC m) (_ : 2 * 4 = 8) //. by rewrite -(addn1 3) addnA addn1 subn1 -pred_Sn. have aux2: forall m, (m ^2) *4 -1 = ((m * 2).+1) * ( (m * 2).-1). case => [// | m]. rewrite aux - (addn1 m) mulnDl mul1n - addnS addn2 -pred_Sn -(addn1 (m*2)). rewrite mulnDl (mulnC 3) mulnDr mulnDl mulnAC // addnA. congr (_ + _);rewrite - addnA ; congr (_ + _); rewrite -!mulnA //- mulnDr. done. have aux3: forall m, (m.+1 * 2).-1 = (m* 2).+1. by move => m;rewrite -(addn1 m) mulnDl mul1n addn2 -pred_Sn. rewrite aux2 aux2 aux3. rewrite mulnCA expnS expn1 -mulnA - mulnDr. symmetry; rewrite mulnA mulnC; congr(_ * _). case: n => [// | n]. rewrite aux3. have ->: (n.+1 * 2).+1 * 3 = (1* (n * 2).+1) + n*4 + 8. rewrite mul1n -(addn1 n) mulnDl -addnS mulnDl mul1n. rewrite - (addn1 (n * 2)) addnAC -addnA -addnA (addnA 1 8) add1n. by rewrite addnCA - mulnDr addnC -mulnA. symmetry; rewrite addnA addnA -mulnDl addn1 -addnA. have ->: (n * 4 + 8) = n.+2 * 4 by rewrite -(addn2 n) mulnDl. rewrite -mulnDr; congr (_ * _). by rewrite addSn - (addn2 n) mulnDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)