proposition: Lemma F6 n: (\sum_(i<n.+1) i ^ 2 ) * 6 = n * (n.+1) * (2*n +1).
proof: Proof. elim: n; first by rewrite big_ord_recl big_ord0 //. move => n Hrec;rewrite big_ord_recr /= mulnDl Hrec. rewrite expnS expn1 (mulnC n) -!mulnA - mulnDr; congr (_ * _). rewrite mulnDr muln1 - (add2n n) - (addn1 n) ! mulnDl mul1n. rewrite 3!mulnDr (mulnA 2) (mulnC 4) -(addnA (n * 4)) (addnAC _ 6). by rewrite addnA -mulnSr - 2!mulnDr addnCA - addnA addSnnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)