proposition: Lemma Grp_modular_group : 'Mod_(p ^ n) \isog Grp (x : y : x ^+ q, y ^+ p, x ^ y = x ^+ r.+1).
proof: Proof. rewrite /modular_gtype def_p def_q def_r; apply: Extremal.Grp => //. set B := <[_]>; have Bb: Zp1 \in B by apply: cycle_id. have oB: #|B| = q by rewrite -orderE order_Zp1 Zp_cast. have cycB: cyclic B by rewrite cycle_cyclic. have pB: p.-group B by rewrite /pgroup oB pnatX ?pnat_id. have ntB: B != 1 by rewrite -cardG_gt1 oB. have [] := cyclic_pgroup_Aut_structure pB cycB ntB. rewrite oB pfactorK //= -/B -(expg_znat r.+1 Bb) oB => mB [[def_mB _ _ _ _] _]. rewrite {1}def_n /= => [[t [At ot mBt]]]. have [p2 | ->] := even_prime p_pr; last first. by case=> _ _ [s [As os mBs _]]; exists s; rewrite os -mBs def_mB. rewrite {1}p2 /= -2!eqSS -addn2 -2!{1}subn1 -subnDA subnK 1?ltnW //. case: eqP => [n3 _ | _ [_ [_ _ _ _ [s [As os mBs _ _]{t At ot mBt}]]]]. by exists t; rewrite At ot -def_mB // mBt /q /r p2 n3. by exists s; rewrite As os -def_mB // mBs /r 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)