proposition: Lemma multinomialE i s : 'C[i :: s] = 'C(i + sumn s, i) * 'C[s].
proof: Proof. by []. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools