proposition: Theorem card_permuted_multinomial : #|[set: permuted w]| = 'C[[seq count_mem x w | x <- undup w]].
proof: Proof. Proof using. rewrite card_permuted multinomial_factd big_map; congr (_`! %/ _). by rewrite sumnE -{1}(size_tuple w) big_map size_count_mem_undup. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles