proposition: Lemma normal_rank1_structure gT p (G : {group gT}) : p.-group G -> (forall X : {group gT}, X <| G -> abelian X -> cyclic X) -> cyclic G \/ [&& p == 2, extremal2 G & (#|G| >= 16) || (G \isog 'Q_8)].
proof: Proof. move=> pG dn_G_1. have [cGG | not_cGG] := boolP (abelian G); first by left; rewrite dn_G_1. have [X maxX]: {X | [max X | X <| G & abelian X]}. by apply: ex_maxgroup; exists 1%G; rewrite normal1 abelian1. have cycX: cyclic X by rewrite dn_G_1; case/andP: (maxgroupp maxX). have scX: X \in 'SCN(G) := max_SCN pG maxX. have [[p2 _ cG] | [M [_ _ _]]] := cyclic_SCN pG scX not_cGG cycX; last first. rewrite 2!inE -andbA => /and3P[sEG abelE dimE_2] charE. have:= dn_G_1 _ (char_normal charE) (abelem_abelian abelE). by rewrite (abelem_cyclic abelE) (eqP dimE_2). have [n oG] := p_natP pG; right; rewrite p2 cG /= in oG *. rewrite oG (@leq_exp2l 2 4) //. rewrite /extremal2 /extremal_class oG pfactorKpdiv // in cG. case: andP cG => [[n_gt1 isoG] _ | _]; last first. by case: (ltngtP 3 n) => //= <-; do 2?case: ifP. have [[x y] genG _] := generators_2dihedral n_gt1 isoG. have [_ _ _ [_ _ maxG]] := dihedral2_structure n_gt1 genG isoG. rewrite 2!ltn_neqAle n_gt1 !(eq_sym _ n). case: eqP => [_ abelG| _]; first by rewrite (abelem_abelian abelG) in not_cGG. case: eqP => // -> [_ _ isoY _ _]; set Y := <<_>> in isoY. have nxYG: Y <| G by rewrite (p_maximal_normal pG) // maxG !inE eqxx orbT. have [// | [u v] genY _] := generators_2dihedral _ isoY. case/dihedral2_structure: (genY) => //= _ _ _ _ abelY. have:= dn_G_1 _ nxYG (abelem_abelian abelY). by rewrite (abelem_cyclic abelY); case: genY => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal)