proposition: Lemma card_isog8_extraspecial (gT : finGroupType) (G : {group gT}) : #|G| = 8 -> extraspecial G -> (G \isog 'D_8) || (G \isog 'Q_8).
proof: Proof. move=> oG esG; have pG: 2.-group G by rewrite /pgroup oG. apply/norP=> [[notG_D8 notG_Q8]]. have not_extG: extremal_class G = NotExtremal. by rewrite /extremal_class oG andFb (negPf notG_D8) (negPf notG_Q8). have [x Gx ox] := exponent_witness (pgroup_nil pG). pose X := <[x]>; have cycX: cyclic X := cycle_cyclic x. have sXG: X \subset G by rewrite cycle_subG. have iXG: #|G : X| = 2. by rewrite -divgS // oG -orderE -ox exponent_2extraspecial. have not_cGG := extraspecial_nonabelian esG. have:= maximal_cycle_extremal pG not_cGG cycX sXG iXG. by rewrite /extremal2 not_extG. Qed.
imports: 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 finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal) mathcomp(extremal)