proposition: Lemma nilpotent_maxp_normal pi G H : nilpotent G -> [max H | pi.-subgroup(G) H] -> H <| G.
proof: Proof. move=> nilG /maxgroupP[/andP[sHG piH] maxH]. have nHN: H <| 'N_G(H) by rewrite normal_subnorm. have{maxH} hallH: pi.-Hall('N_G(H)) H. apply: normal_max_pgroup_Hall => //; apply/maxgroupP. rewrite /psubgroup normal_sub // piH; split=> // K. by rewrite subsetI -andbA andbCA => /andP[_ /maxH]. rewrite /normal sHG; apply/setIidPl/esym. apply: nilpotent_sub_norm; rewrite ?subsetIl ?setIS //= char_norms //. by congr (_ \char _): (pcore_char pi 'N_G(H)); apply: normal_Hall_pcore. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)