proposition: Lemma multinomial1 i : 'C[[:: i]] = 1.
proof: Proof. by rewrite /multinomial /= addn0 muln1 binn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools