proposition: Lemma p2group_abelian P : p.-group P -> logn p #|P| <= 2 -> abelian P.
proof: Proof. move=> pP lePp2; pose Z := 'Z(P); have sZP: Z \subset P := center_sub P. have [/(trivg_center_pgroup pP) ->|] := eqVneq Z 1; first exact: abelian1. case/(pgroup_pdiv (pgroupS sZP pP)) => p_pr _ [k oZ]. apply: cyclic_center_factor_abelian. have [->|] := eqVneq (P / Z) 1; first exact: cyclic1. have pPq := quotient_pgroup 'Z(P) pP; case/(pgroup_pdiv pPq) => _ _ [j oPq]. rewrite prime_cyclic // oPq; case: j oPq lePp2 => //= j. rewrite card_quotient ?gFnorm //. by rewrite -(Lagrange sZP) lognM // => ->; rewrite oZ !pfactorK ?addnS. 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)