proposition: Theorem card_class_perm s : #|class s [set: {perm T}]| = #|T|`! %/ zcard (cycle_type s).
proof: Proof. Proof using. rewrite -card_cent1_perm -index_cent1 /= -divgI. rewrite (eq_card (B := perm_on setT)); first last. move=> p; rewrite inE unfold_in /perm_on /=. by apply/esym/subsetP => i _; rewrite in_set. rewrite card_perm cardsE setTI; congr (_ %/ #|_|). by rewrite /= setTI. 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