proposition: Lemma quaternion_classP : extremal_class G = Quaternion <-> (exists2 n, n > 2 & G \isog 'Q_(2 ^ n)).
proof: Proof. rewrite /extremal_class; split=> [ | [n n_gt2 isoG]]. by move: (logn _ _) => n; do 4?case: ifP => //; case/andP; exists n. rewrite (card_isog isoG) card_quaternion // -(ltn_predK n_gt2) pdiv_pfactor //. rewrite pfactorK // (ltn_predK n_gt2) n_gt2 isoG. case: andP => // [[n_gt1 isoGD]]. have [[x y] genG [oy _ _]]:= generators_quaternion n_gt2 isoG. have [_ _ _ X'y] := genG. by case/dihedral2_structure: genG 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)