proposition: Lemma F8aux n: \sum_(i<n) i ^4 = 'C(n, 2) + 14 * 'C(n, 3) + 36 * 'C(n, 4) + 24 * 'C(n, 5).
proof: Proof. by rewrite sum_pow 5! 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)