proposition: Lemma F7_aux n: n ^ 3 = 6 * 'C(n, 3) + 6 * 'C(n, 2) + 'C(n, 1).
proof: Proof. elim:n => //n Hrec; rewrite - {1} addn1 Pascal 4! big_ord_recr big_ord0 /=. rewrite !exp1n expn0 expn1 !muln1 add0n /subn /= bin0 bin1 mul1n Hrec. rewrite (_: 'C(3, 2) = 3) // !binS !mulnDr bin0 addnA; congr (_ + 1). rewrite - 5!addnA (addnC ('C(n, 1))); congr (_ + (_ + (_ + _))). by rewrite F6_aux mulnDr mulnA bin1 - addnA addnn - mul2n mulnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)