proposition: Lemma generators_quaternion : n > 2 -> G \isog 'Q_m -> exists2 xy, extremal_generators G 2 n xy & let: (x, y) := xy in [/\ #[y] = 4, y ^+ 2 = x ^+ r & x ^ y = x^-1].
proof: Proof. move=> n_gt2; have [def2q def2r ltqm _] := def2qr (ltnW n_gt2). case/(isoGrpP _ (Grp_quaternion n_gt2)); rewrite card_quaternion // -/m => oG. case/existsP=> -[x y] /=; rewrite -/q -/r => /eqP[defG xq y2 xy]. have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. by rewrite dvdn_leq // order_dvdn xq. have ox: #[x] = q. apply/eqP; rewrite eqn_leq dvdn_leq ?order_dvdn ?xq //=. rewrite -(leq_pmul2r (order_gt0 y)) mul_cardG defG oG -def2q mulnAC mulnC. rewrite leq_pmul2r // dvdn_leq ?muln_gt0 ?cardG_gt0 // order_dvdn expgM. by rewrite -order_dvdn order_dvdG //= inE {1}y2 !mem_cycle. have oy2: #[y ^+ 2] = 2 by rewrite y2 orderXdiv ox -def2r ?dvdn_mull ?mulnK. exists (x, y) => /=; last by rewrite (orderXprime oy2). by rewrite oG !inE notXy -!cycle_subG /= -defG mulG_subl mulG_subr. 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)