proposition: Lemma n6bin n: n ^6 = n*'C(n,1) + 30 * n* 'C(n.+1,3) + 120 * n*'C(n.+2,5).
proof: Proof. by rewrite (mulnC 120) (mulnC 30) - 2! mulnA - 2!mulnDr - n5bin expnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)