proposition: Lemma Grp_2dihedral n : n > 1 -> 'D_(2 ^ n) \isog Grp (x : y : x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x^-1).
proof: Proof. move=> n_gt1; rewrite -(ltn_predK n_gt1) expnS mul2n /=. by apply: Grp_dihedral; rewrite (ltn_exp2l 0) // -(subnKC n_gt1). 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)