proposition: Lemma Grp'_dihedral : 'D_m \isog Grp (x : y : x ^+ 2, y ^+ 2, (x * y) ^+ q).
proof: Proof. move=> gT G; rewrite Grp_dihedral; apply/existsP/existsP=> [] [[x y]] /=. case/eqP=> <- xq1 y2 xy; exists (x * y, y); rewrite !xpair_eqE /= eqEsubset. rewrite !join_subG !joing_subr !cycle_subG -{3}(mulgK y x) /=. rewrite 2?groupM ?groupV ?mem_gen ?inE ?cycle_id ?orbT //= -mulgA expgS. by rewrite {1}(conjgC x) xy -mulgA mulKg -(expgS y 1) y2 mulg1 xq1 !eqxx. case/eqP=> <- x2 y2 xyq; exists (x * y, y); rewrite !xpair_eqE /= eqEsubset. rewrite !join_subG !joing_subr !cycle_subG -{3}(mulgK y x) /=. rewrite 2?groupM ?groupV ?mem_gen ?inE ?cycle_id ?orbT //= xyq y2 !eqxx /=. by rewrite eq_sym eq_invg_mul !mulgA mulgK -mulgA -!(expgS _ 1) x2 y2 mulg1. 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)