proposition: Lemma multinomial_nseq n a : 'C[nseq n a] * (a`! ^ n) = (a * n)`!.
proof: Proof. by rewrite -(sumn_nseq a n) -multinomial_fact big_nseq iter_muln_1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools