proposition: Lemma n3bin n: n ^3 = 'C(n,1) + 6 * 'C(n.+1,3).
proof: Proof. rewrite -sum_nbsurj 4! big_ord_recr big_ord0 /= mul0n mul1n 2!add0n - addnA. by rewrite - (mulnDr 6) binS (addnC 'C(n, 2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)