proposition: Corollary card_permuted_multinomial_subset (s : seq T) : {subset w <= s} -> uniq s -> #|[set: permuted w]| = 'C[[seq count_mem x w | x <- s]].
proof: Proof. move=> subws suniq; rewrite card_permuted_multinomial. rewrite -[RHS]multinomial_filter_neq0 filter_map. apply/perm_multinomial/perm_map/uniq_perm; first exact: undup_uniq. exact: filter_uniq. move=> x; rewrite mem_undup mem_filter inE. case: (boolP (x \in w)) => [xinw | /count_memPn ->]; last by rewrite eqxx. rewrite (subws _ xinw) andbT; apply esym. by apply/eqP => /count_memPn; rewrite xinw. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles