proposition: Lemma multinomial2 a b : 'C[[:: a; b]] = 'C(a + b, a).
proof: Proof. by rewrite multinomialE /= addn0 multinomial1 muln1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools