proposition: Lemma card_permuted : #|[set: permuted w]| = n`! %/ \prod_(x <- undup w) (count_mem x w)`!.
proof: Proof. Proof using. by rewrite card_permuted_seq_sub -big_seq_sub. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles