proposition: Lemma modular_group_classP : extremal_class G = ModularGroup <-> (exists2 p, prime p & exists2 n, n >= (p == 2) + 3 & G \isog 'Mod_(p ^ n)).
proof: Proof. rewrite /extremal_class; split=> [ | [p p_pr [n n_gt23 isoG]]]. move: (pdiv _) => p; set n := logn p _; do 4?case: ifP => //. case/andP=> n_gt2 isoG _ _; rewrite ltnW //= => not_isoG _. exists p; first by move: n_gt2; rewrite /n lognE; case (prime p). exists n => //; case: eqP => // p2; rewrite ltn_neqAle; case: eqP => // n3. by case/idP: not_isoG; rewrite p2 -n3 in isoG *. have n_gt2 := leq_trans (leq_addl _ _) n_gt23; have n_gt1 := ltnW n_gt2. have n_gt0 := ltnW n_gt1; have def_n := prednK n_gt0. have [[x y] genG mod_xy] := generators_modular_group p_pr n_gt2 isoG. case/modular_group_structure: (genG) => // _ _ [_ _ nil2G] _ _. have [oG _ _ _] := genG; have [oy _] := mod_xy. rewrite oG -def_n pdiv_pfactor // def_n pfactorK // n_gt1 n_gt2 {}isoG /=. case: (ltngtP p 2) => [|p_gt2|p2]; first by rewrite ltnNge prime_gt1. rewrite !(isog_sym G) !isogEcard card_2dihedral ?card_quaternion //= oG. rewrite leq_exp2r // leqNgt p_gt2 !andbF; case: and3P=> // [[n_gt3 _]]. by rewrite card_semidihedral // leq_exp2r // leqNgt p_gt2. rewrite p2 in genG oy n_gt23; rewrite n_gt23. have: nil_class G <> n.-1. by apply/eqP; rewrite neq_ltn -ltnS nil2G def_n n_gt23. case: ifP => [isoG | _]; first by case/dihedral2_structure: genG => // _ []. case: ifP => [isoG | _]; first by case/quaternion_structure: genG => // _ []. by case: ifP => // isoG; case/semidihedral_structure: genG => // _ []. 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)