proposition: Lemma F7b n: (\sum_(i<n.+1) i ^ 3 ) = 'C(n.+1,2) ^2.
proof: Proof. by rewrite F7aux - addnA - mulnDr (addnC 'C(n.+1, 3)) - binS F7a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)