proposition: Lemma cent1_stab_iporbit_porbitgrpS s : 'C[s] \subset permcycles s @* stab_iporbits s * 'CC(s).
proof: Proof. Proof using. apply/subsetP => t Ht. pose str := permcycles s (inporbits s t^-1). have Hstr : str \in 'C[s] by apply: permcyclesP. rewrite -(mulKg str t); apply mem_mulg. - rewrite groupV /= -/(stab_iporbits s); apply imset_f. by rewrite setIid -inporbits_im; apply imset_f; apply groupVr. - rewrite inE; apply/andP. split; first exact: groupM. apply/astabP => C /imsetP[x _ ->{C}]. rewrite !actM /= cent1_act_porbit //=. rewrite porbit_permcycles; first last. by rewrite -inporbits_im; apply imset_f; apply groupVr. rewrite /inporbits /= restr_permE; first last. + exact: imset_f. + apply/astabsP => X /=; rewrite actpermK. apply astabs_act; move: Ht => /groupVr; apply/subsetP => /=. exact: cent1_act_on_porbits. by rewrite actpermE /= -actM mulVg act1. 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