proposition: Lemma F7aux n: \sum_(i<n) i ^3 = 'C(n, 2) + 6 * 'C(n, 3) + 6 * 'C(n, 4).
proof: Proof. by rewrite sum_pow 4! big_ord_recr /= big_ord0 add0n nbsurjn0 mul0n add0n mul1n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)