proposition: Lemma Grp_ext_dihedral : ED \isog Grp (x : y : x ^+ q, y ^+ p, x ^ y = x^-1).
proof: Proof. suffices isoED: ED \isog Grp (x : y : x ^+ q, y ^+ p, x ^ y = x ^+ q.-1). move=> gT G; rewrite isoED. apply: eq_existsb => [[x y]] /=; rewrite !xpair_eqE. congr (_ && _); apply: andb_id2l; move/eqP=> xq1; congr (_ && (_ == _)). by apply/eqP; rewrite eq_sym eq_invg_mul -expgS (ltn_predK q_gt1) xq1. have unitrN1 : (- 1)%R \in GRing.unit by move=> R; rewrite unitrN unitr1. pose uN1 := FinRing.unit ('Z_#[Zp1 : 'Z_q]) (unitrN1 _). apply: Extremal.Grp => //; exists (Zp_unitm uN1). rewrite Aut_aut order_injm ?injm_Zp_unitm ?in_setT //; split=> //. by rewrite (dvdn_trans _ even_p) // order_dvdn -val_eqE /= mulrNN. apply/eqP; rewrite autE ?cycle_id // eq_expg_mod_order /=. by rewrite order_Zp1 !Zp_cast // !modn_mod (modn_small q_gt1) subn1. 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)