proposition: Lemma multinomial_fact s : 'C[s] * \prod_(i <- s) i`! = (sumn s)`!.
proof: Proof. elim: s => [| i s IHs] /=; first by rewrite fact0 big_nil muln1. rewrite big_cons [i`! * _]mulnC -!mulnA ['C[s] * _]mulnA {}IHs /=. rewrite [_ * i`!]mulnC -{2}(addKn i (sumn s)) bin_fact //. exact: leq_addr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools