proposition: Lemma card_permuted_seq_sub : #|[set: permuted w]| = n`! %/ \prod_(x : seq_sub w) (count_mem (val x) w)`!.
proof: Proof. Proof using. rewrite -card_permuted_prod mulnK //. by apply prodn_gt0 => i; apply: fact_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles