proposition: Lemma im_sdpair_TI : (sdpair1 @* R) :&: (sdpair2 @* D) = 1.
proof: Proof. apply/trivgP; apply/subsetP=> _ /setIP[/morphimP[x _ Rx ->]]. case/morphimP=> a _ Da /eqP; rewrite inE -!val_eqE. by rewrite !val_insubd !inE Da Rx !group1 /eq_op /= eqxx; case/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)