proposition: Lemma multinomial_cat s t : 'C[s ++ t] = 'C(sumn s + sumn t, sumn s) * 'C[s] * 'C[t].
proof: Proof. rewrite !multinomial_factd big_cat sumn_cat /=. rewrite muln_divA ?dvdn_prodfact // [_ * (sumn t)`!]mulnC mulnA. rewrite muln_divA ?dvdn_prodfact // -divnMA -mulnA [(sumn t)`! * _]mulnC. by rewrite -{3}(addKn (sumn s) (sumn t)) -mulnA bin_fact ?leq_addr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools