proposition: Lemma Grp_semidihedral n : n > 3 -> 'SD_(2 ^ n) \isog Grp (x : y : x ^+ (2 ^ n.-1), y ^+ 2, x ^ y = x ^+ (2 ^ n.-2).-1).
proof: Proof. move=> n_gt3. rewrite /('SD__)%type -(subnKC (ltnW (ltnW n_gt3))) pdiv_pfactor //. rewrite !expnS !mulKn // -!expnS /=; set q := (2 ^ _)%N. have q_gt1: q > 1 by rewrite (ltn_exp2l 0). apply: Extremal.Grp => //; set B := <[_]>. have oB: #|B| = q by rewrite -orderE order_Zp1 Zp_cast. have pB: 2.-group B by rewrite /pgroup oB pnatX. have ntB: B != 1 by rewrite -cardG_gt1 oB. have [] := cyclic_pgroup_Aut_structure pB (cycle_cyclic _) ntB. rewrite oB /= pfactorK //= -/B => m [[def_m _ _ _ _] _]. rewrite -{1 2}(subnKC n_gt3) => [[t [At ot _ [s [_ _ _ defA]]]]]. case/dprodP: defA => _ defA cst _. have{cst defA} cAt: t \in 'C(Aut B). rewrite -defA centM inE -sub_cent1 -cent_cycle centsC cst /=. by rewrite cent_cycle cent1id. case=> s0 [As0 os0 _ def_s0t _]; exists (s0 * t). rewrite -def_m ?groupM ?cycle_id // def_s0t !Zp_expg !mul1n valZpK Zp_nat. rewrite order_dvdn expgMn /commute 1?(centP cAt) // -{1}os0 -{1}ot. by rewrite !expg_order mul1g. 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)