proposition: Lemma F7 n: (\sum_(i<n.+1) i ^ 3 ) * 4 = (n * (n.+1)) ^2.
proof: Proof. elim: n; first by rewrite big_ord_recl big_ord0. move => n Hrec;rewrite big_ord_recr /= mulnDl Hrec. rewrite (expnD n.+1 2 1) mulnC 2 !expnMn expn1 -mulnA -mulnDr. by rewrite - (addn2 n) sqrnD mulSn (mulnC 2) - mulnA -addnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)