proposition: Lemma card_p2group_abelian P : prime p -> #|P| = (p ^ 2)%N -> abelian P.
proof: Proof. move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnatX pnat_id. by rewrite (p2group_abelian pP) // oP pfactorK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)