proposition: Lemma im_sdpair_norm : sdpair2 @* D \subset 'N(sdpair1 @* R).
proof: Proof. apply/subsetP=> _ /morphimP[a _ Da ->]. rewrite inE -sdpair_setact // morphimS //. by apply/subsetP=> _ /imsetP[x Rx ->]; rewrite gact_stable. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)