fact: Fixpoint multinomial_rec s := if s is i :: s' then 'C(sumn s, i) * (multinomial_rec s') else 1.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools