proposition: Corollary card_cent1_perm s : #|'C[s]| = zcard (cycle_type s).
proof: Proof. Proof using. have /esym/sdprod_card <- := cent1_permE s. rewrite card_porbitgrpE card_in_imset // ?setIid; first last. by apply: can_in_inj; exact: permcyclesK. by rewrite /zcard card_stab_iporbits // sumn_intpartn. 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