proposition: Lemma semidihedral_classP : extremal_class G = SemiDihedral <-> (exists2 n, n > 3 & G \isog 'SD_(2 ^ n)).
proof: Proof. rewrite /extremal_class; split=> [ | [n n_gt3 isoG]]. by move: (logn _ _) => n; do 4?case: ifP => //; case/andP; exists n. rewrite (card_isog isoG) card_semidihedral //. rewrite -(ltn_predK n_gt3) pdiv_pfactor // pfactorK // (ltn_predK n_gt3) n_gt3. have [[x y] genG [oy _]]:= generators_semidihedral n_gt3 isoG. have [_ Gx _ X'y]:= genG. case: andP => [[n_gt1 isoGD]|_]. have [[_ oxy _ _] _ _ _]:= semidihedral_structure n_gt3 genG isoG oy. case: (dihedral2_structure n_gt1 genG isoGD) oxy => [[_ ->]] //. by rewrite !inE !groupMl ?cycle_id in X'y *. case: andP => // [[n_gt2 isoGQ]|]; last by rewrite isoG. by case: (quaternion_structure n_gt2 genG isoGQ) oy => [[_ ->]]. 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)