proposition: Lemma pgroup_p p P : p.-group P -> p_group P.
proof: Proof. case: (leqP #|P| 1); first by move=> /card_le1_trivg-> _; apply: pgroup1. move/pdiv_prime=> pr_q pgP; have:= pgroupP pgP _ pr_q (pdiv_dvd _). by rewrite /p_group => /eqnP->. 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)