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