proposition: Lemma restr_perm_porbits S s : restr_perm S s \in 'C(porbits s | ('P)^* ).
proof: Proof. Proof using. have [nSs | /triv_restr_perm -> //] := (boolP (s \in 'N(S | 'P))). apply/astabP => /= X /imsetP[x _ ->{X}]. case: (boolP (x \in S)) => Hx. - apply/setP => y; apply/imsetP/idP => [[z Hz ->{y}] /= | Hy]. + have:= Hz; rewrite -eq_porbit_mem => /eqP Hsz. rewrite apermE restr_permE //. - rewrite -Hsz -{1}(expg1 s); exact: mem_porbit. - by rewrite (stab_porbit nSs) // Hsz -stab_porbit. + have HsVy : s^-1 y \in porbit s x. by rewrite porbit_sym -(porbit_perm _ 1) expg1 permKV porbit_sym. exists ((s ^-1) y); first exact: HsVy. rewrite /= apermE restr_permE => //; first by rewrite permKV. by move: Hx; rewrite (stab_porbit nSs) => /subsetP; apply. - move: nSs; rewrite -astabsC => nSs. have: x \in ~: S by rewrite inE. rewrite (stab_porbit nSs) => Hsubs. apply/setP => y; apply/imsetP/idP => [[z Hz ->{y}] /= | Hy]. + rewrite apermE (out_perm (restr_perm_on _ _)) //. by have:= subsetP Hsubs z Hz; rewrite inE. + exists y; first exact Hy. rewrite /= apermE (out_perm (restr_perm_on _ _)) //. by have:= subsetP Hsubs y Hy; rewrite inE. 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