proposition: Lemma multinomial_nseq1 n : 'C[nseq n 1] = n`!.
proof: Proof. by have:= multinomial_nseq n 1; rewrite exp1n muln1 mul1n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools