proposition: Lemma normal_max_pgroup_Hall G H : [max H | pi.-subgroup(G) H] -> H <| G -> pi.-Hall(G) H.
proof: Proof. case/maxgroupP=> /andP[sHG piH] maxH nsHG; have [_ nHG] := andP nsHG. rewrite /pHall sHG piH; apply/pnatP=> // p p_pr. rewrite inE /= -pnatE // -card_quotient //. case/Cauchy=> //= Hx; rewrite -sub1set -gen_subG -/<[Hx]> /order. case/inv_quotientS=> //= K -> sHK sKG {Hx}. rewrite card_quotient ?(subset_trans sKG) // => iKH; apply/negP=> pi_p. rewrite -iKH -divgS // (maxH K) ?divnn ?cardG_gt0 // in p_pr. by rewrite /psubgroup sKG /pgroup -(Lagrange sHK) mulnC pnatM iKH pi_p. 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)