proposition: Lemma card_pgroup p G : p.-group G -> #|G| = (p ^ logn p #|G|)%N.
proof: Proof. by move=> pG; rewrite -p_part part_pnat_id. 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)