proposition: Lemma Grp_pX1p2 : p^{1+2} \isog Grp (x : y : x ^+ p, y ^+ p, [~ x, y, x], [~ x, y, y]).
proof: Proof. rewrite [@gtype _]unlock; apply: intro_isoGrp => [|rT H]. apply/existsP; pose x := sdpair1 actp (0, 1)%R; pose y := sdpair2 actp 1%R. exists (x, y); rewrite /= !xpair_eqE; set z := [~ x, y]; set G := _ <*> _. have def_z: z = sdpair1 actp (1, 0)%R. rewrite [z]commgEl -sdpair_act ?inE //=. rewrite -morphV -?morphM ?inE //=; congr (sdpair1 _ (_, _)) => /=. by rewrite mulr1 mulKg. by rewrite mulVg. have def_xi i: x ^+ i = sdpair1 actp (0, i%:R)%R. rewrite -morphX ?inE //; congr (sdpair1 _ _). by apply/eqP; rewrite /eq_op /= !morphX ?inE ?expg1n //=. have def_yi i: y ^+ i = sdpair2 actp i%:R. by rewrite -morphX ?inE //. have def_zi i: z ^+ i = sdpair1 actp (i%:R, 0)%R. rewrite def_z -morphX ?inE //; congr (sdpair1 _ _). by apply/eqP; rewrite /eq_op /= !morphX ?inE ?expg1n ?andbT //=. rewrite def_xi def_yi char_Zp ?morph1 //. rewrite def_z -morphR ?inE // !commgEl -sdpair_act ?inE //= mulr0 addr0. rewrite mulVg -[_ * _]/(_ , _) /= !invg1 mulg1 !mul1g mulVg morph1 !andbT. have Gx: x \in G by rewrite -cycle_subG joing_subl. have Gy: y \in G by rewrite -cycle_subG joing_subr. rewrite eqEsubset subsetT -im_sdpair mulG_subG /= -/G; apply/andP; split. apply/subsetP=> u /morphimP[[i j] _ _ def_u]. suffices ->: u = z ^+ i * x ^+ j by rewrite groupMl groupX ?groupR. rewrite def_zi def_xi !natr_Zp -morphM ?inE // def_u. by congr (sdpair1 _ (_, _)); rewrite ?mulg1 ?mul1g. apply/subsetP=> v /morphimP[k _ _ def_v]. suffices ->: v = y ^+ k by rewrite groupX. by rewrite def_yi natr_Zp. case/existsP=> [[x y] /=]; set z := [~ x, y]. case/eqP=> defH xp yp /eqP/commgP czx /eqP/commgP czy. have zp: z ^+ p = 1 by rewrite -commXg // xp comm1g. pose f1 (ij : 'Z_p * 'Z_p) := let: (i, j) := ij in z ^+ i * x ^+ j. have f1M: {in setT &, {morph f1 : u v / u * v}}. case=> /= [i1 j1] [i2 j2] _ _ /=; rewrite {3 6}Zp_cast // !expg_mod //. rewrite !expgD !mulgA; congr (_ * _); rewrite -!mulgA; congr (_ * _). by apply: commuteX2. pose f2 (k : 'Z_p) := y ^+ k. have f2M: {in setT &, {morph f2 : u v / u * v}}. by move=> k1 k2 _ _; rewrite /f2 /= {3}Zp_cast // expg_mod // expgD. have actf: {in setT & setT, morph_act actp 'J (Morphism f1M) (Morphism f2M)}. case=> /= i j k _ _; rewrite modnDmr {4}Zp_cast // expg_mod // expgD. rewrite /f2 conjMg {1}/conjg (commuteX2 i k czy) mulKg -mulgA. congr (_ * _); rewrite (commuteX2 _ _ czx) mulnC expgM. by rewrite -commXg // -commgX ?mulKVg // commXg // /commute commuteX. apply/homgP; exists (xsdprod_morphism actf). apply/eqP; rewrite eqEsubset -{2}defH -genM_join gen_subG /= im_xsdprodm. have Hx: x \in H by rewrite -cycle_subG -defH joing_subl. have Hy: y \in H by rewrite -cycle_subG -defH joing_subr. rewrite mulG_subG -andbA; apply/and3P; split. - apply/subsetP=> _ /morphimP[[i j] _ _ -> /=]. by rewrite groupMl groupX ?groupR. - by apply/subsetP=> _ /morphimP[k _ _ ->]; rewrite groupX. rewrite mulgSS ?cycle_subG //= morphimEdom; apply/imsetP. by exists (0, 1)%R; rewrite ?inE //= mul1g. by exists 1%R; rewrite ?inE. 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)