proposition: Lemma SylowP G P : reflect (exists2 p, prime p & p.-Sylow(G) P) (Sylow G P).
proof: Proof. apply: (iffP idP) => [| [p _]]; last exact: p_Sylow. case/andP=> /p_groupP[p p_pr] /p_natP[[P1 _ | n oP /Hall_pi]]; last first. by rewrite /= oP pi_of_exp // (eq_pHall _ _ (pi_of_prime _)) //; exists p. have{p p_pr P1} ->: P :=: 1 by apply: card1_trivg; rewrite P1. pose p := pdiv #|G|.+1; have p_pr: prime p by rewrite pdiv_prime ?ltnS. exists p; rewrite // pHallE sub1G cards1 part_p'nat //. apply/pgroupP=> q pr_q qG; apply/eqnP=> def_q. have: p %| #|G| + 1 by rewrite addn1 pdiv_dvd. by rewrite dvdn_addr -def_q // Euclid_dvd1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)