proposition: Lemma normal_sylowP G : reflect (exists2 P : {group gT}, p.-Sylow(G) P & P <| G) (#|'Syl_p(G)| == 1%N).
proof: Proof. apply: (iffP idP) => [syl1 | [P sylP nPG]]; last first. by rewrite (card_Syl sylP) (setIidPl _) (indexgg, normal_norm). have [P sylP] := Sylow_exists p G; exists P => //. rewrite /normal (pHall_sub sylP); apply/setIidPl; apply/eqP. rewrite eqEcard subsetIl -(LagrangeI G 'N(P)) -indexgI /=. by rewrite -(card_Syl sylP) (eqP syl1) muln1. 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)