proposition: Lemma prime_Ohm1P gT p (G : {group gT}) : p.-group G -> G :!=: 1 -> reflect (#|'Ohm_1(G)| = p) (cyclic G || (p == 2) && (extremal_class G == Quaternion)).
proof: Proof. move=> pG ntG; have [p_pr p_dvd_G _] := pgroup_pdiv pG ntG. apply: (iffP idP) => [|oG1p]. case/orP=> [cycG|]; first exact: Ohm1_cyclic_pgroup_prime. case/andP=> /eqP p2 /eqP/quaternion_classP[n n_gt2 isoG]. rewrite p2; have [[x y]] := generators_quaternion n_gt2 isoG. by case/quaternion_structure=> // _ _ [<- oZ _ [->]]. have [X nsXG cXX|-> //|]:= normal_rank1_structure pG. have [sXG _] := andP nsXG; have pX := pgroupS sXG pG. rewrite abelian_rank1_cyclic // (rank_pgroup pX) p_rank_abelian //. rewrite -{2}(pfactorK 1 p_pr) -{3}oG1p dvdn_leq_log ?cardG_gt0 //. by rewrite cardSg ?OhmS. case/and3P=> /eqP p2; rewrite p2 (orbC (cyclic G)) /extremal2. case cG: (extremal_class G) => //; case: notF. case/dihedral_classP: cG => n n_gt1 isoG. have [[x y] genG _] := generators_2dihedral n_gt1 isoG. have [oG _ _ _] := genG; case/dihedral2_structure: genG => // _ _ [defG1 _] _. by case/idPn: n_gt1; rewrite -(@ltn_exp2l 2) // -oG -defG1 oG1p p2. case/semidihedral_classP: cG => n n_gt3 isoG. have [[x y] genG [oy _]] := generators_semidihedral n_gt3 isoG. case/semidihedral_structure: genG => // _ _ [_ _ [defG1 _] _] _ [isoG1 _ _]. case/idPn: (n_gt3); rewrite -(ltn_predK n_gt3) ltnS -leqNgt -(@leq_exp2l 2) //. rewrite -card_2dihedral //; last by rewrite -(subnKC n_gt3). by rewrite -(card_isog isoG1) /= -defG1 oG1p p2. 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)