proposition: Lemma pprod_norm_coprime_prod : 'C_K(H) * 'N_U(H) = 'N_G(H).
proof: Proof. apply/eqP; rewrite eqEsubset mul_subG ?setISS ?cent_sub //=. apply/subsetP=> g /setIP[Gg /normP nHg]. have [|c Cc [u Uu defg]] := pprod_trans_coprime Gg; first by rewrite nHg. rewrite defg mem_mulg // !inE Uu -{2}nHg defg conjsgM conjSg (normP _) //=. by case/setIP: Cc => _; apply: (subsetP (cent_sub H)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)