proposition: Lemma F11aux n: \sum_(i<n) i ^7 = 'C(n, 2) + (63 * 2) * 'C(n, 3) + (301 * 3`!) * 'C(n, 4) + (350 * 4`!) * 'C(n, 5) + (140 * 5`!) * 'C(n, 6) + (21 * 6`!) * 'C(n, 7) + 7`! * 'C(n, 8).
proof: Proof. by rewrite sum_pow 8! big_ord_recr /= big_ord0 mul0n mul1n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)