proposition: Lemma astabEsd : 'C(G | to) = sdpair2 @*^-1 'C(sdpair1 @* G).
proof: Proof. have ssGR := subsetP sGR; apply/setP=> a; apply/idP/idP=> [cGa|]. rewrite mem_morphpre ?(astab_dom cGa) //. apply/centP=> _ /morphimP[x Rx Gx ->]; symmetry. by rewrite conjgC -sdpair_act ?(astab_act cGa) ?(astab_dom cGa). case/morphpreP=> Da cGa; rewrite !inE Da; apply/subsetP=> x Gx; rewrite inE. apply/eqP; apply: (injmP injm_sdpair1); rewrite ?gact_stable ?ssGR //=. by rewrite sdpair_act ?ssGR // /conjg -(centP cGa) ?mulKg ?mem_morphim ?ssGR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)