proposition: Theorem extremal2_structure (gT : finGroupType) (G : {group gT}) n x y : let cG := extremal_class G in let m := (2 ^ n)%N in let q := (2 ^ n.-1)%N in let r := (2 ^ n.-2)%N in let X := <[x]> in let yG := y ^: G in let xyG := (x * y) ^: G in let My := <<yG>> in let Mxy := <<xyG>> in extremal_generators G 2 n (x, y) -> extremal2 G -> (cG == SemiDihedral) ==> (#[y] == 2) -> [/\ [/\ (if cG == Quaternion then pprod X <[y]> else X ><| <[y]>) = G, if cG == SemiDihedral then #[x * y] = 4 else {in G :\: X, forall z, #[z] = (if cG == Dihedral then 2 else 4)}, if cG != Quaternion then True else {in G, forall z, #[z] = 2 -> z = x ^+ r} & {in X & G :\: X, forall t z, t ^ z = (if cG == SemiDihedral then t ^+ r.-1 else t^-1)}], [/\ G ^`(1) = <[x ^+ 2]>, 'Phi(G) = G ^`(1), #|G^`(1)| = r & nil_class G = n.-1], [/\ if n > 2 then 'Z(G) = <[x ^+ r]> /\ #|'Z(G)| = 2 else 2.-abelem G, 'Ohm_1(G) = (if cG == Quaternion then <[x ^+ r]> else if cG == SemiDihedral then My else G), 'Ohm_2(G) = G & forall k, k > 0 -> 'Mho^k(G) = <[x ^+ (2 ^ k)]>], [/\ yG :|: xyG = G :\: X, [disjoint yG & xyG] & forall H : {group gT}, maximal H G = (gval H \in pred3 X My Mxy)] & if n <= (cG == Quaternion) + 2 then True else [/\ forall U, cyclic U -> U \subset G -> #|G : U| = 2 -> U = X, if cG == Quaternion then My \isog 'Q_q else My \isog 'D_q, extremal_class My = (if cG == Quaternion then cG else Dihedral), if cG == Dihedral then Mxy \isog 'D_q else Mxy \isog 'Q_q & extremal_class Mxy = (if cG == Dihedral then cG else Quaternion)]].
proof: Proof. move=> cG m q r X yG xyG My Mxy genG; have [oG _ _ _] := genG. have logG: logn (pdiv #|G|) #|G| = n by rewrite oG pfactorKpdiv. rewrite /extremal2 -/cG; do [rewrite {1}/extremal_class /= {}logG] in cG *. case: ifP => [isoG | _] in cG * => [_ _ /=|]. case/andP: isoG => n_gt1 isoG. have:= dihedral2_structure n_gt1 genG isoG; rewrite -/X -/q -/r -/yG -/xyG. case=> [[defG oX' invXX'] nilG [defOhm defMho] maxG defZ]. rewrite eqn_leq n_gt1 andbT add0n in defZ *; split=> //. split=> //; first by case: leqP defZ => // _ []. by apply/eqP; rewrite eqEsubset Ohm_sub -{1}defOhm Ohm_leq. case: leqP defZ => // n_gt2 [_ _ isoMy isoMxy defX]. have n1_gt1: n.-1 > 1 by rewrite -(subnKC n_gt2). by split=> //; apply/dihedral_classP; exists n.-1. case: ifP => [isoG | _] in cG * => [_ _ /=|]. case/andP: isoG => n_gt2 isoG; rewrite n_gt2 add1n. have:= quaternion_structure n_gt2 genG isoG; rewrite -/X -/q -/r -/yG -/xyG. case=> [[defG oX' invXX'] nilG [defZ oZ def2 [-> ->] defMho]]. case=> [[-> ->] maxG] isoM; split=> //. case: leqP isoM => // n_gt3 [//|isoMy isoMxy defX]. have n1_gt2: n.-1 > 2 by rewrite -(subnKC n_gt3). by split=> //; apply/quaternion_classP; exists n.-1. do [case: ifP => [isoG | _]; last by case: ifP] in cG * => /= _; move/eqnP=> oy. case/andP: isoG => n_gt3 isoG; rewrite (leqNgt n) (ltnW n_gt3) /=. have n1_gt2: n.-1 > 2 by rewrite -(subnKC n_gt3). have:= semidihedral_structure n_gt3 genG isoG oy. rewrite -/X -/q -/r -/yG -/xyG -/My -/Mxy. case=> [[defG oxy invXX'] nilG [defZ oZ [-> ->] defMho] [[defX' tiX'] maxG]]. case=> isoMy isoMxy defX; do 2!split=> //. by apply/dihedral_classP; exists n.-1; first apply: ltnW. by apply/quaternion_classP; exists n.-1. 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)