proposition: Lemma sdpair2_morphM : {in D &, {morph sdpair2 : a b / a * b}}.
proof: Proof. move=> a b Da Db; apply: val_inj. by rewrite /= !val_insubd !inE !group1 !groupM ?Da ?Db //= mulg1 gact1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)