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