proposition: Lemma nilpotent_Hall_pcore pi G H : nilpotent G -> pi.-Hall(G) H -> H :=: 'O_pi(G).
proof: Proof. move=> nilG hallH; have maxH := Hall_max hallH; apply/eqP. rewrite eqEsubset pcore_max ?(pHall_pgroup hallH) //. by rewrite (normal_sub_max_pgroup maxH) ?pcore_pgroup ?pcore_normal. exact: nilpotent_maxp_normal maxH. 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)