proposition: Lemma im_sdpair : (sdpair1 @* R) * (sdpair2 @* D) = setT.
proof: Proof. apply/eqP; rewrite -subTset -(normC im_sdpair_norm). apply/subsetP=> /= u _; rewrite [u]sdpairE. by case: u => [[a x] /= /setXP[Da Rx]]; rewrite mem_mulg ?mem_morphim. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)