proposition: Lemma generators_modular_group gT (G : {group gT}) : G \isog 'Mod_m -> exists2 xy, extremal_generators G p n xy & modular_group_generators xy.
proof: Proof. case/(isoGrpP _ Grp_modular_group); rewrite card_modular_group // -/m => oG. case/existsP=> -[x y] /= /eqP[defG xq yp xy]. rewrite norm_joinEr ?norms_cycle ?xy ?mem_cycle // in defG. have [Gx Gy]: x \in G /\ y \in G. by apply/andP; rewrite -!cycle_subG -mulG_subG defG. have notXy: y \notin <[x]>. apply: contraL ltqm; rewrite -cycle_subG -oG -defG; move/mulGidPl->. by rewrite -leqNgt dvdn_leq ?(ltnW q_gt1) // order_dvdn xq. have oy: #[y] = p by apply: nt_prime_order (group1_contra notXy). exists (x, y) => //=; split; rewrite ?inE ?notXy //. apply/eqP; rewrite -(eqn_pmul2r p_gt0) -expnSr -{1}oy (ltn_predK n_gt2) -/m. by rewrite -TI_cardMg ?defG ?oG // setIC prime_TIg ?cycle_subG // -orderE 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)