proposition: Lemma isog_2X1p2 : 2^{1+2} \isog 'D_8.
proof: Proof. have pr2: prime 2 by []; have oG := card_pX1p2 pr2; rewrite -[8]oG. case/existsP: (isoGrp_hom (Grp_pX1p2 pr2)) => [[x y]] /=. rewrite -/2^{1+2}; case/eqP=> defG x2 y2 _ _. have not_oG_2: ~~ (#|2^{1+2}| %| 2) by rewrite oG. have ox: #[x] = 2. apply: nt_prime_order => //; apply: contra not_oG_2 => x1. by rewrite -defG (eqP x1) cycle1 joing1G order_dvdn y2. have oy: #[y] = 2. apply: nt_prime_order => //; apply: contra not_oG_2 => y1. by rewrite -defG (eqP y1) cycle1 joingG1 order_dvdn x2. rewrite -defG joing_idl joing_idr involutions_gen_dihedral //. apply: contra not_oG_2 => eq_xy; rewrite -defG (eqP eq_xy) (joing_idPl _) //. by rewrite -orderE oy. Qed.
imports: 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 finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal) mathcomp(extremal)