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