proposition: Lemma sdpair1_morphM : {in R &, {morph sdpair1 : x y / x * y}}.
proof: Proof. move=> x y Rx Ry; apply: val_inj. by rewrite /= !val_insubd !inE !group1 !groupM ?Rx ?Ry //= mulg1 act1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)