proposition: Lemma card_stab_iporbits s : #|stab_iporbits s| = (\prod_(i < #|T|.+1) (count_mem (nat_of_ord i) (cycle_type s))`!)%N.
proof: Proof. Proof using. rewrite -(bigdprod_card (esym (stab_iporbitsE s))). apply eq_bigr => i _. rewrite card_Sym /setpart_shape; congr (_)`!. have /permPl/seq.permP -> := perm_sort geq [seq #{x} | x in porbits s]. rewrite !cardE -size_filter /= /enum_mem. rewrite filter_map size_map -filter_predI; congr size. by apply eq_filter => C; rewrite !inE andbC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype