proposition: Lemma Grp : (exists s, [/\ s \in Aut B, #[s] %| p & s b = b ^+ e]) -> [set: gtype] \isog Grp (x : y : x ^+ q, y ^+ p, x ^ y = x ^+ e).
proof: Proof. rewrite [gtype.body]unlock => [[s [AutBs dvd_s_p sb]]]. have memB: _ \in B by move=> c; rewrite -Zp_cycle inE. have Aa: a \in <[a]> by rewrite !cycle_id. have [oa ob]: #[a] = p /\ #[b] = q by rewrite !order_Zp1 !Zp_cast. have def_s: aut_of = s. rewrite /aut_of; case: pickP => /= [t | ]; last first. by move/(_ s); case/and4P; rewrite sb. case/and4P=> AutBt _ _ tb; apply: (eq_Aut AutBt) => // b_i. case/cycleP=> i ->; rewrite -(autmE AutBt) -(autmE AutBs) !morphX //=. by rewrite !autmE // sb (eqP tb). apply: intro_isoGrp => [|gT G]. apply/existsP; exists (sdpair1 _ b, sdpair2 _ a); rewrite /= !xpair_eqE. rewrite -!morphim_cycle ?norm_joinEr ?im_sdpair ?im_sdpair_norm ?eqxx //=. rewrite -!order_dvdn !order_injm ?injm_sdpair1 ?injm_sdpair2 // oa ob !dvdnn. by rewrite -sdpair_act // [act _ _ _]apermE /= eltm_id -morphX // -sb -def_s. case/existsP=> -[x y] /= /eqP[defG xq1 yp1 xy]. have fxP: #[x] %| #[b] by rewrite order_dvdn ob xq1. have fyP: #[y] %| #[a] by rewrite order_dvdn oa yp1. have fP: {in <[b]> & <[a]>, morph_act gact 'J (eltm fxP) (eltm fyP)}. move=> bj ai; case/cycleP=> j ->{bj}; case/cycleP=> i ->{ai}. rewrite /= !eltmE def_s gactX ?groupX // conjXg morphX //=; congr (_ ^+ j). rewrite /autact /= apermE; elim: i {j} => /= [|i IHi]. by rewrite perm1 eltm_id conjg1. rewrite !expgS permM sb -(autmE (groupX i AutBs)) !morphX //= {}IHi. by rewrite -conjXg -xy -conjgM. apply/homgP; exists (xsdprod_morphism fP). rewrite im_xsdprodm !morphim_cycle //= !eltm_id -norm_joinEr //. by rewrite norms_cycle xy mem_cycle. 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)