proposition: Lemma remgrM : K <| G -> {in G &, {morph remgr K H : x y / x * y}}.
proof: Proof. case/normalP=> _; case/complP: complH_K => tiKH <- nK_KH x y KHx KHy. rewrite {1}(divgr_eq K H y) mulgA (conjgCV x) {2}(divgr_eq K H x) -2!mulgA. rewrite mulgA remgrMid //; last by rewrite groupMl mem_remgr. by rewrite groupMl !(=^~ mem_conjg, nK_KH, mem_divgr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)