proposition: Lemma generators_2dihedral : n > 1 -> G \isog 'D_m -> exists2 xy, extremal_generators G 2 n xy & let: (x, y) := xy in #[y] = 2 /\ x ^ y = x^-1.
proof: Proof. move=> n_gt1; have [def2q _ ltqm _] := def2qr n_gt1. case/(isoGrpP _ (Grp_2dihedral n_gt1)); rewrite card_2dihedral // -/ m => oG. case/existsP=> -[x y] /=; rewrite -/q => /eqP[defG xq y2 xy]. have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. by rewrite dvdn_leq // order_dvdn xq. have oy: #[y] = 2 by apply: nt_prime_order (group1_contra notXy). have ox: #[x] = q. apply: double_inj; rewrite -muln2 -oy -mul2n def2q -oG -defG TI_cardMg //. by rewrite setIC prime_TIg ?cycle_subG // -orderE oy. exists (x, y) => //=. by rewrite oG ox !inE notXy -!cycle_subG /= -defG mulG_subl mulG_subr. 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)