proposition: Lemma card_porbitgrpE s : #|'CC(s)| = (\prod_(i <- cycle_type s) i)%N.
proof: Proof. Proof using. rewrite -(bigdprod_card (esym (porbitgrpE s))). rewrite /cycle_type /= /setpart_shape /cycle_dec. rewrite big_imset /=; last exact: restr_perm_inj. rewrite [RHS](perm_big [seq #{x} | x in porbits s]); last by apply/permPl; apply perm_sort. rewrite /= [RHS]big_map big_enum. rewrite [RHS](bigID (fun X => #{X} == 1%N)) /=. rewrite [X in _ = (X * _)%N]big1 ?mul1n; last by move=> i /andP[_ /eqP]. rewrite [RHS](eq_bigl (mem (porbit_set s))) /=; last by move=> C; rewrite /porbit_set !inE. apply eq_bigr => X HX; rewrite -orderE. rewrite order_cyclic; last by rewrite unfold_in (porbit_set_restr HX) cards1. by rewrite psupport_restr_perm. 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