proposition: Lemma Sylow_subnorm p G P : p.-Sylow('N_G(P)) P = p.-Sylow(G) P.
proof: Proof. apply/idP/idP=> sylP; last first. apply: pHall_subl (subsetIl _ _) (sylP). by rewrite subsetI normG (pHall_sub sylP). have [/subsetIP[sPG sPN] pP _] := and3P sylP. have [Q sylQ sPQ] := Sylow_superset sPG pP; have [sQG pQ _] := and3P sylQ. rewrite -(nilpotent_sub_norm (pgroup_nil pQ) sPQ) {sylQ}//. rewrite subEproper eq_sym eqEcard subsetI sPQ sPN dvdn_leq //. rewrite -(part_pnat_id (pgroupS (subsetIl _ _) pQ)) (card_Hall sylP). by rewrite partn_dvd // cardSg ?setSI. 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)