proposition: Lemma F9aux n: \sum_(i<n) i ^5 = 'C(n, 2) + 30 * 'C(n, 3) + 150 * 'C(n, 4) + 240 * 'C(n, 5) + 120 * 'C(n, 6).
proof: Proof. by rewrite sum_pow 6! 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)