proposition: Lemma card_permuted_prod : #|[set: permuted w]| * \prod_(x : seq_sub w) (count_mem (val x) w)`! = n`!.
proof: Proof. Proof using. rewrite -card_Sn -card_stab_tuple. rewrite -(atransPin (subxx _) permuted_action_trans (x := wp)) ?inE //. by rewrite -cardsT /= -(card_orbit_in_stab pact wp (subxx _)) /= setTI. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles