proposition: Lemma xsdprodm_act : {in DgH & DgK, morph_act 'J 'J gH gK}.
proof: Proof. move=> fh fk; case/morphimP=> h _ Hh ->{fh}; case/morphimP=> k _ Kk ->{fk}. by rewrite /= -sdpair_act // /restrm /= !invmE ?actf ?gact_stable. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)