proposition: Lemma Hall_Frattini_arg pi (G K H : {group gT}) : solvable K -> K <| G -> pi.-Hall(K) H -> K * 'N_G(H) = G.
proof: Proof. move=> solK /andP[sKG nKG] hallH. have sHG: H \subset G by apply: subset_trans sKG; case/andP: hallH. rewrite setIC group_modl //; apply/setIidPr/subsetP=> x Gx. pose H1 := (H :^ x^-1)%G. have hallH1: pi.-Hall(K) H1 by rewrite pHallJnorm // groupV (subsetP nKG). case: (Hall_trans solK hallH hallH1) => y Ky defH. rewrite -(mulKVg y x) mem_mulg //; apply/normP. by rewrite conjsgM {1}defH conjsgK conjsgKV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)