proposition: Lemma F9aux2 n: \sum_(i<n) i ^5 = 'C(n, 6) + 26* 'C(n + 1, 6) + 66 * 'C(n + 2, 6) + 26 * 'C(n + 3, 6) + 'C(n + 4, 6).
proof: Proof. rewrite sum_pow_euler 5! big_ord_recr /= big_ord0 2! mul1n addn0 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)