proposition: Lemma critical_p_stab_Aut H : critical H G -> p.-group G -> p.-group 'C(H | [Aut G]).
proof: Proof. move=> [chH sPhiZ sRZ eqCZ] pG; have sHG := char_sub chH. pose G' := (sdpair1 [Aut G] @* G)%G; pose H' := (sdpair1 [Aut G] @* H)%G. apply/pgroupP=> q pr_q; case/Cauchy=> //= f cHF; move: (cHF); rewrite astab_ract. case/setIP=> Af cHFP ofq; rewrite -cycle_subG in cHF; apply: (pgroupP pG) => //. pose F' := (sdpair2 [Aut G] @* <[f]>)%G. have trHF: [~: H', F'] = 1. apply/trivgP; rewrite gen_subG; apply/subsetP=> u; case/imset2P=> x' a'. case/morphimP=> x Gx Hx ->; case/morphimP=> a Aa Fa -> -> {u x' a'}. by rewrite inE commgEl -sdpair_act ?(astab_act (subsetP cHF _ Fa) Hx) ?mulVg. have sGH_H: [~: G', H'] \subset H'. by rewrite -morphimR ?(char_sub chH) // morphimS // commg_subr char_norm. have{trHF sGH_H} trFGH: [~: F', G', H'] = 1. apply: three_subgroup; last by rewrite trHF comm1G. by apply/trivgP; rewrite -trHF commSg. apply/negP=> qG; case: (qG); rewrite -ofq. suffices ->: f = 1 by rewrite order1 dvd1n. apply/permP=> x; rewrite perm1; case Gx: (x \in G); last first. by apply: out_perm (negbT Gx); case/setIdP: Af. have Gfx: f x \in G by rewrite -(im_autm Af) -{1}(autmE Af) mem_morphim. pose y := x^-1 * f x; have Gy: y \in G by rewrite groupMl ?groupV. have [inj1 inj2] := (injm_sdpair1 [Aut G], injm_sdpair2 [Aut G]). have Hy: y \in H. rewrite (subsetP (center_sub H)) // -eqCZ -cycle_subG. rewrite -(injmSK inj1) ?cycle_subG // injm_subcent // subsetI. rewrite morphimS ?morphim_cycle ?cycle_subG //=. suffices: sdpair1 [Aut G] y \in [~: G', F']. by rewrite commGC; apply: subsetP; apply/commG1P. rewrite morphM ?groupV ?morphV //= sdpair_act // -commgEl. by rewrite mem_commg ?mem_morphim ?cycle_id. have fy: f y = y := astabP cHFP _ Hy. have: (f ^+ q) x = x * y ^+ q. elim: (q) => [|i IHi]; first by rewrite perm1 mulg1. rewrite expgSr permM {}IHi -(autmE Af) morphM ?morphX ?groupX //= autmE. by rewrite fy expgS mulgA mulKVg. move/eqP; rewrite -{1}ofq expg_order perm1 eq_mulVg1 mulKg -order_dvdn. case/primeP: pr_q => _ pr_q /pr_q; rewrite order_eq1 -eq_mulVg1. by case: eqP => //= _ /eqP oyq; case: qG; rewrite -oyq order_dvdG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)