proposition: Lemma multinomial_factd s : 'C[s] = (sumn s)`! %/ \prod_(i <- s) i`!.
proof: Proof. rewrite -multinomial_fact mulnK //. by apply prodn_gt0 => i; apply fact_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools