proposition: Lemma pprodmM : {in H <*> K &, {morph f: x y / x * y}}.
proof: Proof. move=> xa yb; rewrite norm_joinEr //. move=> /imset2P[x a Ha Ka ->{xa}] /imset2P[y b Hy Kb ->{yb}]. have Hya: y ^ a^-1 \in H by rewrite -mem_conjg (normsP nHK). rewrite mulgA -(mulgA x) (conjgCV a y) (mulgA x) -mulgA !pprodmE 1?groupMl //. by rewrite morphM // actf ?groupV ?morphV // morphM // !mulgA mulgKV invgK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)