proposition: Lemma card_stab_tuple : #|('C[wp | pact])%G| = \prod_(x : seq_sub w) (count_mem (val x) w)`!.
proof: Proof. Proof using. rewrite -(bigdprod_card (esym stab_tuple_dprod)). apply eq_bigr => [[i _]] _ /=. rewrite card_Sym; congr (_)`!. rewrite -map_tnth_enum. rewrite cardE /enum_mem size_filter /= count_map count_filter. by apply eq_count => X; rewrite !inE andbC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles