proposition: Lemma divgrM : H \subset 'C(K) -> {in G &, {morph divgr K H : x y / x * y}}.
proof: Proof. move=> cKH; have /complP[_ defG] := complH_K. have nsKG: K <| G by rewrite -defG -cent_joinEr // normalYl cents_norm. move=> x y Gx Gy; rewrite {1}/divgr remgrM // invMg -!mulgA (mulgA y). by congr (_ * _); rewrite -(centsP cKH) ?groupV ?(mem_remgr, mem_divgr, defG). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)