proposition: Lemma sdpair_setact (G : {set rT}) a : G \subset R -> a \in D -> sdpair1 @* (to^~ a @: G) = (sdpair1 @* G) :^ sdpair2 a.
proof: Proof. move=> sGR Da; have GtoR := subsetP sGR; apply/eqP. rewrite eqEcard cardJg !(card_injm injm_sdpair1) //; last first. by apply/subsetP=> _ /imsetP[x Gx ->]; rewrite gact_stable ?GtoR. rewrite (card_imset _ (act_inj _ _)) leqnn andbT. apply/subsetP=> _ /morphimP[xa Rxa /imsetP[x Gx def_xa ->]]. rewrite mem_conjg -morphV // -sdpair_act ?groupV // def_xa actKin //. by rewrite mem_morphim ?GtoR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)