proposition: Lemma uniq_normal_Hall pi H G K : pi.-Hall(G) H -> H <| G -> [max K | pi.-subgroup(G) K] -> K :=: H.
proof: Proof. move=> hallH nHG /maxgroupP[/andP[sKG piK] /(_ H) -> //]. exact: (maxgroupp (Hall_max hallH)). by rewrite (sub_normal_Hall hallH). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)