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