proposition: Lemma porbitgrpE s : 'CC(s) = \big[dprod/1]_(c in cycle_dec s) <[c]>.
proof: Proof. Proof using. rewrite disjoint_psupport_dprodE; last exact: disjoint_cycle_dec. apply/setP => /= t; apply/idP/idP. - rewrite inE => /andP[Hcomm Hstab]. have:= partition_psupport s => /and3P[/eqP Hcov Htriv _]. rewrite -(perm_decE (S := porbit_set s) (s := t)) //; first last. + by apply/astabP => C; rewrite /porbit_set inE => /andP[/(astabP Hstab)]. + rewrite {}Hcov; apply/subsetP => x. rewrite !in_psupport (porbit_fix s); apply contra => /eqP Hx. have /(astabP Hstab) : porbit s x \in porbits s by apply: imset_f. rewrite Hx => /setP/(_ x). rewrite inE eq_refl /= => /imsetP[y]. by rewrite inE => /eqP -> /=; rewrite apermE => <-. + rewrite /cycle_dec bigprodGE. apply/group_prod => c /imsetP[C HC ->{c}]. apply mem_gen; apply/bigcupP; exists (restr_perm C s). * by rewrite /perm_dec; apply/imsetP; exists C. * by apply: restr_perm_genC; rewrite // inE Hcomm Hstab. - rewrite bigprodGEgen; apply /subsetP; rewrite gen_subG. apply/subsetP => /= x /bigcupP[/= c /imsetP[/= C HC ->{c}]]. move: HC; rewrite 3!inE => /andP[HC _] /eqP ->{x}. apply/andP; split. + by apply/cent1P; apply: restr_perm_commute. + exact: restr_perm_porbits. 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