proposition: Lemma p_groupP P : p_group P -> exists2 p, prime p & p.-group P.
proof: Proof. case: (ltnP 1 #|P|); first by move/pdiv_prime; exists (pdiv #|P|). by move/card_le1_trivg=> -> _; exists 2 => //; apply: pgroup1. 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)