proposition: Lemma nilpotent_pcore_Hall pi G : nilpotent G -> pi.-Hall(G) 'O_pi(G).
proof: Proof. move=> nilG; case: (@maxgroup_exists _ (psubgroup pi G) 1) => [|H maxH _]. by rewrite /psubgroup sub1G pgroup1. have hallH := normal_max_pgroup_Hall maxH (nilpotent_maxp_normal nilG maxH). by rewrite -(nilpotent_Hall_pcore nilG hallH). 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)