proposition: Lemma F6' n: (\sum_(i<n.+1) i ^ 2 ) * 6 = n * (n.+1) * (n.*2.+1).
proof: Proof. rewrite F6aux mulnDl mulnAC (_: 2 * 6 = 4 * 3) // (_: 6 = 2 * 3) //. rewrite mulnA bin2' - (mulnA 4) - mul_bin_diag mulnCA (mulnC 4); case: n => // n. rewrite (_: 4 = 2 * 2) // (mulnA _ 2) bin2' (mulnC n) -(mulnA _ n) mulnA. by rewrite (mulnC n.+2) - mulnDr - muln2 (mulSn _ 2) addSn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)