proposition: Lemma astabsEsd : 'N(G | to) = sdpair2 @*^-1 'N(sdpair1 @* G).
proof: Proof. apply/setP=> a; apply/idP/idP=> [nGa|]. have Da := astabs_dom nGa; rewrite mem_morphpre // inE sub_conjg. apply/subsetP=> _ /morphimP[x Rx Gx ->]. by rewrite mem_conjgV -sdpair_act // mem_morphim ?gact_stable ?astabs_act. case/morphpreP=> Da nGa; rewrite !inE Da; apply/subsetP=> x Gx. have Rx := subsetP sGR _ Gx; have Rxa: to x a \in R by rewrite gact_stable. rewrite inE -sub1set -(injmSK injm_sdpair1) ?morphim_set1 ?sub1set //=. by rewrite sdpair_act ?memJ_norm ?mem_morphim. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)