proposition: Lemma involutions_gen_dihedral gT (x y : gT) : let G := <<[set x; y]>> in #[x] = 2 -> #[y] = 2 -> x != y -> G \isog 'D_#|G|.
proof: Proof. move=> G ox oy ne_x_y; pose q := #[x * y]. have q_gt1: q > 1 by rewrite order_gt1 -eq_invg_mul invg_expg ox. have homG: G \homg 'D_q.*2. rewrite Grp'_dihedral //; apply/existsP; exists (x, y); rewrite /= !xpair_eqE. by rewrite joing_idl joing_idr -{1}ox -oy !expg_order !eqxx. suff oG: #|G| = q.*2 by rewrite oG isogEcard oG card_dihedral ?leqnn ?andbT. have: #|G| %| q.*2 by rewrite -card_dihedral ?card_homg. have Gxy: <[x * y]> \subset G. by rewrite cycle_subG groupM ?mem_gen ?set21 ?set22. have[k oG]: exists k, #|G| = (k * q)%N by apply/dvdnP; rewrite cardSg. rewrite oG -mul2n dvdn_pmul2r ?order_gt0 ?dvdn_divisors // !inE /=. case/pred2P=> [k1 | -> //]; case/negP: ne_x_y. have cycG: cyclic G. apply/cyclicP; exists (x * y); apply/eqP. by rewrite eq_sym eqEcard Gxy oG k1 mul1n leqnn. have: <[x]> == <[y]>. by rewrite (eq_subG_cyclic cycG) ?genS ?subsetUl ?subsetUr -?orderE ?ox ?oy. by rewrite eqEcard cycle_subG /= cycle2g // !inE -order_eq1 ox; case/andP. 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)