proposition: Proposition rank2_exponent_p_p3group gT (R : {group gT}) p : p.-group R -> rank R <= 2 -> exponent R %| p -> logn p #|R| <= 3.
proof: Proof. move=> pR rankR expR. have [A max_na_A]: {A | [max A | A <| R & abelian A]}. by apply: ex_maxgroup; exists 1%G; rewrite normal1 abelian1. have {max_na_A} SCN_A := max_SCN pR max_na_A. have cAA := SCN_abelian SCN_A; case/SCN_P: SCN_A => nAR cRAA. have sAR := normal_sub nAR; have pA := pgroupS sAR pR. have abelA : p.-abelem A. by rewrite /abelem pA cAA /= (dvdn_trans (exponentS sAR) expR). have cardA : logn p #|A| <= 2. by rewrite -rank_abelem // (leq_trans (rankS sAR) rankR). have cardRA : logn p #|R : A| <= 1. by rewrite -cRAA logn_quotient_cent_abelem // (normal_norm nAR). rewrite -(Lagrange sAR) lognM ?cardG_gt0 //. by apply: (leq_trans (leq_add cardA cardRA)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)