proposition: Lemma perm_multinomial s t : perm_eq s t -> 'C[s] = 'C[t].
proof: Proof. rewrite !multinomial_factd => Hperm. by rewrite (perm_sumn Hperm) (perm_big _ Hperm). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(bigop div binomial) tools