proposition: Lemma F9' n (a := 'C(n.+1,2)): (\sum_(i<n.+1) i ^ 5 ) * 3 = a * a * (4*a -1).
proof: Proof. apply /eqP; rewrite - (eqn_pmul2r (ltn0Sn 3)) - mulnA F9; apply /eqP. rewrite (mulnAC n) - (mulnA _ n) - mulnDl - mulnSr - (mulnA 2). rewrite (mulnC _ n) - bin2' -/a (mulnC _ 2) (mulnA 2 2) (mulnC _ 4). by rewrite - (mulnA 2) (mulnCA a 2) mulnA - mulnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)