proposition: Lemma gacentEsd : 'C_(|to)(A) = sdpair1 @*^-1 'C(sdpair2 @* A).
proof: Proof. apply/setP=> x; apply/idP/idP. case/setIP=> Rx /afixP cDAx; rewrite mem_morphpre //. apply/centP=> _ /morphimP[a Da Aa ->]; red. by rewrite conjgC -sdpair_act // cDAx // inE Da. case/morphpreP=> Rx cAx; rewrite inE Rx; apply/afixP=> a /setIP[Da Aa]. apply: (injmP injm_sdpair1); rewrite ?gact_stable /= ?sdpair_act //=. by rewrite /conjg (centP cAx) ?mulKg ?mem_morphim. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)