proposition: Lemma pgroup_pdiv p G : p.-group G -> G :!=: 1 -> [/\ prime p, p %| #|G| & exists m, #|G| = p ^ m.+1]%N.
proof: Proof. move=> pG; rewrite trivg_card1; case/p_groupP: (pgroup_p pG) => q q_pr qG. move/implyP: (pgroupP pG q q_pr); case/p_natP: qG => // [[|m] ->] //. by rewrite dvdn_exp // => /eqnP <- _; split; rewrite ?dvdn_exp //; exists m. 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)