move odd_order to its own repository

1 files changed, 0 insertions, 1123 deletions

diff --git a/mathcomp/odd_order/BGsection13.v b/mathcomp/odd_order/BGsection13.v
deleted file mode 100644
index de9ddaf..0000000
--- a/mathcomp/odd_order/BGsection13.v
+++ /dev/null
@@ -1,1123 +0,0 @@
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq div path fintype.
-From mathcomp
-Require Import bigop finset prime fingroup morphism perm automorphism quotient.
-From mathcomp
-Require Import action gproduct gfunctor pgroup cyclic center commutator.
-From mathcomp
-Require Import gseries nilpotent sylow abelian maximal hall frobenius.
-From mathcomp
-Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
-From mathcomp
-Require Import BGsection7 BGsection9 BGsection10 BGsection12.
-
-(******************************************************************************)
-(*   This file covers B & G, section 13; the title subject of the section,    *)
-(* prime and regular actions, was defined in the frobenius.v file.            *)
-(******************************************************************************)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Import GroupScope.
-
-Section Section13.
-
-Variable gT : minSimpleOddGroupType.
-Local Notation G := (TheMinSimpleOddGroup gT).
-Implicit Types p q q_star r : nat.
-Implicit Types A E H K L M Mstar N P Q Qstar R S T U V W X Y Z : {group gT}.
-
-Section OneComplement.
-
-Variables M E : {group gT}.
-Hypotheses (maxM : M \in 'M) (hallE : \sigma(M)^'.-Hall(M) E).
-
-Let sEM : E \subset M := pHall_sub hallE.
-Let sM'E : \sigma(M)^'.-group E := pHall_pgroup hallE.
-
-(* This is B & G, Lemma 13.1. *)
-Lemma Msigma_setI_mmax_central p H :
-   H \in 'M -> p \in \pi(E) -> p \in \pi(H) -> p \notin \tau1(H) ->
-   [~: M`_\sigma :&: H, M :&: H] != 1 -> gval H \notin M :^: G ->
- [/\ (*a*) forall P, P \subset M :&: H -> p.-group P ->
-           P \subset 'C(M`_\sigma :&: H),
-     (*b*) p \notin \tau2(H)
-   & (*c*) p \in \tau1(M) -> p \in \beta(G)].
-Proof.
-move=> maxH piEp piHp t1H'p; set R := [~: _, _] => ntR notMGH.
-have [q sMq piH'q]: exists2 q, q \in \sigma(M) & q \in \pi(H^`(1)).
-  pose q := pdiv #|R|; have q_pr: prime q by rewrite pdiv_prime ?cardG_gt1.
-  have q_dv : q %| _ := dvdn_trans (pdiv_dvd _) (cardSg _).
-  exists q; last by rewrite mem_primes q_pr cardG_gt0 q_dv ?commgSS ?subsetIr.
-  rewrite (pgroupP (pcore_pgroup _ M)) ?q_dv //.
-  have sR_MsM: R \subset [~: M`_\sigma, M] by rewrite commgSS ?subsetIl.
-  by rewrite (subset_trans sR_MsM) // commg_subl gFnorm.
-have [Y sylY] := Sylow_exists q H^`(1); have [sYH' qY _] := and3P sylY.
-have nsHbH: H`_\beta <| H := pcore_normal _ _; have [_ nHbH] := andP nsHbH.
-have sYH := subset_trans sYH' (der_sub 1 H); have nHbY := subset_trans sYH nHbH.
-have nsHbY_H: H`_\beta <*> Y <| H.
-  rewrite -{2}(quotientGK nsHbH) -quotientYK ?cosetpre_normal //.
-  have ->: Y / H`_\beta = 'O_q(H^`(1) / H`_\beta).
-     by apply: nilpotent_Hall_pcore; rewrite ?Mbeta_quo_nil ?quotient_pHall.
-  by rewrite quotient_der ?gFnormal_trans.
-have sYNY: Y \subset 'N_H(Y) by rewrite subsetI sYH normG.
-have{nsHbY_H} defH: H`_\beta * 'N_H(Y) = H.
-  rewrite -(mulSGid sYNY) mulgA -(norm_joinEr nHbY).
-  rewrite (Frattini_arg _ (pHall_subl _ _ sylY)) ?joing_subr //.
-  by rewrite join_subG Mbeta_der1.
-have ntY: Y :!=: 1 by rewrite -cardG_gt1 (card_Hall sylY) p_part_gt1.
-have{ntY} [_] := sigma_Jsub maxM (pi_pgroup qY sMq) ntY.
-have maxY_H: H \in 'M(Y) by apply/setIdP.
-move/(_ E p H hallE piEp _ maxY_H notMGH) => b'p_t3Hp.
-case t2Hp: (p \in \tau2(H)).
-  have b'p: p \notin \beta(G) by case/tau2_not_beta: t2Hp.
-  have rpH: 'r_p(H) = 2 by apply/eqP; case/andP: t2Hp.
-  have p'Hb: p^'.-group H`_\beta.
-    rewrite (pi_p'group (pcore_pgroup _ H)) // inE /=.
-    by rewrite -predI_sigma_beta // negb_and b'p orbT.
-  case: b'p_t3Hp; rewrite // -(p_rank_p'quotient p'Hb) ?subIset ?nHbH //=.
-  by rewrite -quotientMidl defH p_rank_p'quotient ?rpH.
-have [S sylS] := Sylow_exists p H; have [sSH pS _] := and3P sylS.
-have sSH': S \subset H^`(1).
-  have [sHp | sH'p] := boolP (p \in \sigma(H)).
-    apply: subset_trans (Msigma_der1 maxH).
-    by rewrite (sub_Hall_pcore (Msigma_Hall _)) // (pi_pgroup pS).
-  have sH'_S: \sigma(H)^'.-group S by rewrite (pi_pgroup pS).
-  have [F hallF sSF] := Hall_superset (mmax_sol maxH) sSH sH'_S.
-  have t3Hp: p \in \tau3(H).
-    have:= partition_pi_sigma_compl maxH hallF p.
-    by rewrite (pi_sigma_compl hallF) inE /= sH'p piHp (negPf t1H'p) t2Hp.
-  have [[F1 hallF1] [F3 hallF3]] := ex_tau13_compl hallF.
-  have [F2 _ complFi] := ex_tau2_compl hallF hallF1 hallF3.
-  have [[sF3F' nsF3F] _ _ _ _] := sigma_compl_context maxH complFi.
-  apply: subset_trans (subset_trans sF3F' (dergS 1 (pHall_sub hallF))).
-  by rewrite (sub_normal_Hall hallF3) ?(pi_pgroup pS).
-have sylS_H' := pHall_subl sSH' (der_sub 1 H) sylS.
-split=> // [P sPMH pP | t1Mp]; last first.
-  apply/idPn=> b'p; have [_ /(_ t1Mp)/negP[]] := b'p_t3Hp b'p.
-  have p'Hb: p^'.-group H`_\beta.
-    rewrite (pi_p'group (pcore_pgroup _ H)) // inE /=.
-    by rewrite -predI_sigma_beta // negb_and b'p orbT.
-  rewrite -p_rank_gt0 -(p_rank_p'quotient p'Hb) ?comm_subG ?subIset ?nHbH //=.
-  rewrite quotient_der ?subIset ?nHbH // -quotientMidl defH -quotient_der //=.
-  rewrite p_rank_p'quotient ?comm_subG // -(rank_Sylow sylS_H').
-  by rewrite (rank_Sylow sylS) p_rank_gt0.
-have nsHaH: H`_\alpha <| H := pcore_normal _ _; have [_ nHaH] := andP nsHaH.
-have [sPM sPH] := subsetIP sPMH; have nHaS := subset_trans sSH nHaH.
-have nsHaS_H: H`_\alpha <*> S <| H.
-  rewrite -[H in _ <| H](quotientGK nsHaH) -quotientYK ?cosetpre_normal //.
-  have ->: S / H`_\alpha = 'O_p(H^`(1) / H`_\alpha).
-    by apply: nilpotent_Hall_pcore; rewrite ?Malpha_quo_nil ?quotient_pHall.
-  by rewrite quotient_der ?gFnormal_trans.
-have [sHaS_H nHaS_H] := andP nsHaS_H.
-have sP_HaS: P \subset H`_\alpha <*> S.
-  have [x Hx sPSx] := Sylow_subJ sylS sPH pP; apply: subset_trans sPSx _.
-  by rewrite sub_conjg (normsP nHaS_H) ?groupV ?joing_subr.
-have coHaS_Ms: coprime #|H`_\alpha <*> S| #|M`_\sigma|.
-  rewrite (p'nat_coprime _ (pcore_pgroup _ _)) // -pgroupE norm_joinEr //.
-  rewrite pgroupM andbC (pi_pgroup pS) ?(pnatPpi (pHall_pgroup hallE)) //=.
-  apply: sub_pgroup (pcore_pgroup _ _) => r aHr.
-  have [|_ ti_aH_sM _] := sigma_disjoint maxH maxM; first by rewrite orbit_sym.
-  by apply: contraFN (ti_aH_sM r) => sMr; apply/andP.
-rewrite (sameP commG1P trivgP) -(coprime_TIg coHaS_Ms) commg_subI ?setIS //.
-by rewrite subsetI sP_HaS (subset_trans sPM) ?gFnorm.
-Qed.
-
-(* This is B & G, Corollary 13.2. *)
-Corollary cent_norm_tau13_mmax p P H :
-    (p \in \tau1(M)) || (p \in \tau3(M)) ->
-    P \subset M -> p.-group P -> H \in 'M('N(P)) ->
- [/\ (*a*) forall P1, P1 \subset M :&: H -> p.-group P1 ->
-           P1 \subset 'C(M`_\sigma :&: H),
-     (*b*) forall X, X \subset E :&: H -> \tau1(H)^'.-group X ->
-           X \subset 'C(M`_\sigma :&: H)
-   & (*c*) [~: M`_\sigma :&: H, M :&: H] != 1 ->
-           p \in \sigma(H) /\ (p \in \tau1(M) -> p \in \beta(H))].
-Proof.
-move=> t13Mp sPM pP /setIdP[maxH sNP_H].
-have ntP: P :!=: 1.
-  by apply: contraTneq sNP_H => ->; rewrite norm1 proper_subn ?mmax_proper.
-have st2Hp: (p \in \sigma(H)) || (p \in \tau2(H)).
-  exact: (prime_class_mmax_norm maxH pP sNP_H).
-have not_MGH: gval H \notin M :^: G.
-  apply: contraL st2Hp => /imsetP[x _ ->]; rewrite sigmaJ tau2J negb_or.
-  by have:= t13Mp; rewrite -2!andb_orr !inE => /and3P[-> /eqP->].
-set R := [~: _, _]; have [/commG1P | ntR] := altP (R =P 1).
-  rewrite centsC => cMH; split=> // X sX_EH _; apply: subset_trans cMH => //.
-  by rewrite (subset_trans sX_EH) ?setSI.
-have piEp: p \in \pi(E).
-  by rewrite (partition_pi_sigma_compl maxM) // orbCA t13Mp orbT.
-have piHp: p \in \pi(H).
-  by rewrite (partition_pi_mmax maxH) orbCA orbC -!orbA st2Hp !orbT.
-have t1H'p: p \notin \tau1(H).
-  by apply: contraL st2Hp; rewrite negb_or !inE => /and3P[-> /eqP->].
-case: (Msigma_setI_mmax_central maxH piEp) => // cMsH t2H'p b_p.
-split=> // [X sX_EH t1'X | _].
-  have [sXE sXH] := subsetIP sX_EH.
-  rewrite -(Sylow_gen X) gen_subG; apply/bigcupsP=> Q; case/SylowP=> q _ sylQ.
-  have [-> | ntQ] := eqsVneq Q 1; first exact: sub1G.
-  have piXq: q \in \pi(X) by rewrite -p_rank_gt0 -(rank_Sylow sylQ) rank_gt0.
-  have [[piEq piHq] t1H'q] := (piSg sXE piXq, piSg sXH piXq, pnatPpi t1'X piXq).
-  have [sQX qQ _] := and3P sylQ; have sXM := subset_trans sXE sEM.
-  case: (Msigma_setI_mmax_central maxH piEq) => // -> //.
-  by rewrite subsetI !(subset_trans sQX).
-rewrite (negPf t2H'p) orbF in st2Hp.
-by rewrite -predI_sigma_beta // {3}/in_mem /= st2Hp.
-Qed.
-
-(* This is B & G, Corollary 13.3(a). *)
-Lemma cyclic_primact_Msigma p P :
-  p.-Sylow(E) P -> cyclic P -> semiprime M`_\sigma P.
-Proof.
-move=> sylP cycP x /setD1P[]; rewrite -cycle_eq1 -cycle_subG => ntX sXP.
-have [sPE pP _] := and3P sylP; rewrite -cent_cycle.
-have sPM := subset_trans sPE sEM; have sXM := subset_trans sXP sPM.
-have pX := pgroupS sXP pP; have ltXG := mFT_pgroup_proper pX.
-have t13p: (p \in \tau1(M)) || (p \in \tau3(M)).
-  rewrite (tau1E maxM hallE) (tau3E maxM hallE) -p_rank_gt0 -(rank_Sylow sylP).
-  rewrite eqn_leq rank_gt0 (subG1_contra sXP) //= andbT -andb_orl orNb.
-  by rewrite -abelian_rank1_cyclic ?cyclic_abelian.
-have [H maxNH] := mmax_exists (mFT_norm_proper ntX ltXG).
-have [cMsX _ _] := cent_norm_tau13_mmax t13p sXM pX maxNH.
-have [_ sNH] := setIdP maxNH.
-apply/eqP; rewrite eqEsubset andbC setIS ?centS // subsetI subsetIl /= centsC.
-apply: subset_trans (cMsX P _ pP) (centS _).
-  rewrite subsetI sPM (subset_trans (cents_norm _) sNH) //.
-  by rewrite sub_abelian_cent // cyclic_abelian.
-by rewrite setIS // (subset_trans (cent_sub _) sNH).
-Qed.
-
-(* This is B & G, Corollary 13.3(b). *)
-Corollary tau3_primact_Msigma E3 :
-  \tau3(M).-Hall(E) E3 -> semiprime M`_\sigma E3.
-Proof.
-move=> hallE3 x /setD1P[]; rewrite -cycle_eq1 -cycle_subG => ntX sXE3.
-have [sE3E t3E3 _] := and3P hallE3; rewrite -cent_cycle.
-have [[E1 hallE1] _] := ex_tau13_compl hallE.
-have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3.
-have [[sE3E' nsE3E] _ [_ cycE3] _ _] := sigma_compl_context maxM complEi.
-apply/eqP; rewrite eqEsubset andbC setIS ?centS // subsetI subsetIl /= centsC.
-pose p := pdiv #[x]; have p_pr: prime p by rewrite pdiv_prime ?cardG_gt1.
-have t3p: p \in \tau3(M) by rewrite (pgroupP (pgroupS sXE3 t3E3)) ?pdiv_dvd.
-have t13p: [|| p \in \tau1(M) | p \in \tau3(M)] by rewrite t3p orbT.
-have [y Xy oy]:= Cauchy p_pr (pdiv_dvd _).
-have ntY: <[y]> != 1 by rewrite -cardG_gt1 -orderE oy prime_gt1.
-have pY: p.-group <[y]> by rewrite /pgroup -orderE oy pnat_id.
-have [H maxNH] := mmax_exists (mFT_norm_proper ntY (mFT_pgroup_proper pY)).
-have sYE3: <[y]> \subset E3 by rewrite cycle_subG (subsetP sXE3).
-have sYE := subset_trans sYE3 sE3E; have sYM := subset_trans sYE sEM.
-have [_ cMsY _] := cent_norm_tau13_mmax t13p sYM pY maxNH.
-have [_ sNH] := setIdP maxNH.
-have sE3H': E3 \subset H^`(1).
-  rewrite (subset_trans sE3E') ?dergS // (subset_trans _ sNH) ?normal_norm //.
-  by rewrite (char_normal_trans _ nsE3E) // sub_cyclic_char.
-apply: subset_trans (cMsY E3 _ _) (centS _).
-- rewrite subsetI sE3E (subset_trans (cents_norm _) sNH) //.
-  by rewrite sub_abelian_cent ?cyclic_abelian.
-- rewrite (pgroupS sE3H') //; apply/pgroupP=> q _ q_dv_H'.
-  by rewrite !inE q_dv_H' !andbF.
-by rewrite setIS // (subset_trans _ sNH) // cents_norm ?centS ?cycle_subG.
-Qed.
-
-(* This is B & G, Theorem 13.4. *)
-(* Note how the non-structural steps in the proof (top of p. 99, where it is  *)
-(* deduced that C_M_alpha(P) <= C_M_alpha(R) from q \notin \alpha, and then   *)
-(* C_M_alpha(P) = C_M_alpha(R) from r \in tau_1(M) !!), are handled cleanly   *)
-(* on lines 5-12 of the proof by a conditional expression for the former, and *)
-(* a without loss tactic for the latter.                                      *)
-(*   Also note that the references to 10.12 and 12.2 are garbled (some are    *)
-(* missing, and some are exchanged!).                                         *)
-Theorem cent_tau1Elem_Msigma p r P R (Ms := M`_\sigma) :
-    p \in \tau1(M) -> P \in 'E_p^1(E) -> R \in 'E_r^1('C_E(P)) ->
-  'C_Ms(P) \subset 'C_Ms(R).
-Proof.
-have /andP[sMsM nMsM]: Ms <| M := pcore_normal _ M.
-have coMsE: coprime #|Ms| #|E| := coprime_sigma_compl hallE.
-pose Ma := M`_\alpha; have sMaMs: Ma \subset Ms := Malpha_sub_Msigma maxM.
-rewrite pnElemI -setIdE => t1Mp EpP /setIdP[ErR cPR].
-without loss symPR: p r P R EpP ErR cPR t1Mp /
-  r \in \tau1(M) -> 'C_Ma(P) \subset 'C_Ma(R) -> 'C_Ma(P) = 'C_Ma(R).
-- move=> IH; apply: (IH p r) => // t1Mr sCaPR; apply/eqP; rewrite eqEsubset.
-  rewrite sCaPR -(setIidPl sMaMs) -!setIA setIS ?(IH r p) 1?centsC // => _.
-  by case/eqVproper; rewrite // /proper sCaPR andbF.
-do [rewrite !subsetI !subsetIl /=; set cRCaP := _ \subset _] in symPR *.
-pose Mz := 'O_(if cRCaP then \sigma(M) else \alpha(M))(M); pose C := 'C_Mz(P).
-suffices: C \subset 'C(R) by rewrite /C /Mz /cRCaP; case: ifP => // ->.
-have sMzMs: Mz \subset Ms by rewrite /Mz; case: ifP => // _.
-have sCMs: C \subset Ms by rewrite subIset ?sMzMs.
-have [[sPE abelP dimP] [sRE abelR dimR]] := (pnElemP EpP, pnElemP ErR).
-have [sPM sRM] := (subset_trans sPE sEM, subset_trans sRE sEM).
-have [[pP cPP _] [rR _]] := (and3P abelP, andP abelR).
-have coCR: coprime #|C| #|R| := coprimeSg sCMs (coprimegS sRE coMsE).
-have ntP: P :!=: 1 by apply: nt_pnElem EpP _.
-pose ST := [set S | Sylow C (gval S) & R \subset 'N(S)].
-have sST_CP S: S \in ST -> S \subset C by case/setIdP=> /SylowP[q _ /andP[]].
-rewrite -{sST_CP}[C](Sylow_transversal_gen sST_CP)  => [|q _]; last first.
-  have nMzR: R \subset 'N(Mz) by rewrite (subset_trans sRM) // gFnorm.
-  have{nMzR} nCR: R \subset 'N(C) by rewrite normsI // norms_cent // cents_norm.
-  have solC := solvableS (subset_trans sCMs sMsM) (mmax_sol maxM).
-  have [S sylS nSR] := coprime_Hall_exists q nCR coCR solC.
-  by exists S; rewrite // inE (p_Sylow sylS) nSR.
-rewrite gen_subG; apply/bigcupsP=> S /setIdP[/SylowP[q _ sylS] nSR] {ST}.
-have [sSC qS _] := and3P sylS.
-have [sSMs [sSMz cPS]] := (subset_trans sSC sCMs, subsetIP sSC).
-rewrite (sameP commG1P eqP) /=; set Q := [~: S, R]; apply/idPn => ntQ.
-have sQS: Q \subset S by [rewrite commg_subl]; have qQ := pgroupS sQS qS.
-have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 -(rank_pgroup qQ) rank_gt0.
-have{piQq} [nQR piSq] := (commg_normr R S : R \subset 'N(Q), piSg sQS piQq).
-have [H maxNH] := mmax_exists (mFT_norm_proper ntP (mFT_pgroup_proper pP)).
-have [maxH sNH] := setIdP maxNH; have sCPH := subset_trans (cent_sub _) sNH.
-have [sPH sRH] := (subset_trans cPP sCPH, subset_trans cPR sCPH).
-have [sSM sSH] := (subset_trans sSMs sMsM, subset_trans cPS sCPH).
-have [sQM sQH] := (subset_trans sQS sSM, subset_trans sQS sSH).
-have ntMsH_R: [~: Ms :&: H, R] != 1.
-  by rewrite (subG1_contra _ ntQ) ?commSg // subsetI sSMs.
-have sR_EH: R \subset E :&: H by apply/subsetIP.
-have ntMsH_MH: [~: Ms :&: H, M :&: H] != 1.
-  by rewrite (subG1_contra _ ntMsH_R) ?commgS // (subset_trans sR_EH) ?setSI.
-have t13Mp: p \in [predU \tau1(M) & \tau3(M)] by apply/orP; left.
-have [_ cMsH_t1H' [//|sHp bHp]] := cent_norm_tau13_mmax t13Mp sPM pP maxNH.
-have{cMsH_t1H'} t1Hr: r \in \tau1(H).
-  apply: contraR ntMsH_R => t1H'r; rewrite (sameP eqP commG1P) centsC.
-  by rewrite cMsH_t1H' // (pi_pgroup rR).
-have ntCHaRQ: 'C_(H`_\alpha)(R <*> Q) != 1.
-  rewrite centY (subG1_contra _ ntP) ?subsetI //= centsC cPR centsC.
-  rewrite (subset_trans sQS cPS) (subset_trans _ (Mbeta_sub_Malpha H)) //.
-  by rewrite (sub_Hall_pcore (Mbeta_Hall maxH)) // (pi_pgroup pP) ?bHp.
-have not_MGH: gval H \notin M :^: G.
-  by apply: contraL sHp => /imsetP[x _ ->]; rewrite sigmaJ; case/andP: t1Mp.
-have neqHM: H :!=: M := contra_orbit _ _ not_MGH.
-have cSS: abelian S.
-  apply: contraR neqHM => /(nonabelian_Uniqueness qS)uniqS.
-  by rewrite (eq_uniq_mmax (def_uniq_mmax uniqS maxM sSM) maxH sSH).
-have tiQcR: 'C_Q(R) = 1 by rewrite coprime_abel_cent_TI // (coprimeSg sSC).
-have sMq: q \in \sigma(M) := pnatPpi (pcore_pgroup _ M) (piSg sSMs piSq).
-have aH'q: q \notin \alpha(H).
-  have [|_ tiHaMs _] := sigma_disjoint maxH maxM; first by rewrite orbit_sym.
-  by apply: contraFN (tiHaMs q) => aHq; apply/andP.
-have piRr: r \in \pi(R) by rewrite -p_rank_gt0 p_rank_abelem ?dimR.
-have ErH_R: R \in 'E_r^1(H) by rewrite !inE sRH abelR dimR.
-have{piRr} sM'r: r \in \sigma(M)^' := pnatPpi (pgroupS sRE sM'E) piRr.
-have r'q: q \in r^' by apply: contraTneq sMq => ->.
-have ntHa: H`_\alpha != 1 by rewrite (subG1_contra _ ntCHaRQ) ?subsetIl.
-have uniqNQ: 'M('N(Q)) = [set H].
-  apply: contraNeq ntCHaRQ; rewrite joingC.
-  by case/(cent_Malpha_reg_tau1 _ _ r'q ErH_R) => //; case=> //= _ -> _.
-have maxNQ_H: H \in 'M('N(Q)) :\ M by rewrite uniqNQ !inE neqHM /=.
-have{maxNQ_H} [_ _] := sigma_subgroup_embedding maxM sMq sQM qQ ntQ maxNQ_H.
-have [sHq [_ st1HM [_ ntMa]] | _ [_ _ sM'MH]] := ifP; last first.
-  have piPp: p \in \pi(P) by rewrite -p_rank_gt0 p_rank_abelem ?dimP.
-  have sPMH: P \subset M :&: H by apply/subsetIP.
-  by have/negP[] := pnatPpi (pgroupS sPMH (pHall_pgroup sM'MH)) piPp.
-have{st1HM} t1Mr: r \in \tau1(M).
-  by case/orP: (st1HM r t1Hr); rewrite //= (contraNF ((alpha_sub_sigma _) r)).
-have aM'q: q \notin \alpha(M).
-  have [_ tiMaHs _] := sigma_disjoint maxM maxH not_MGH.
-  by apply: contraFN (tiMaHs q) => aMq; apply/andP.
-have ErM_R: R \in 'E_r^1(M) by rewrite !inE sRM abelR dimR.
-have: 'M('N(Q)) != [set M] by rewrite uniqNQ (inj_eq (@set1_inj _)).
-case/(cent_Malpha_reg_tau1 _ _ r'q ErM_R) => //.
-case=> //= ntCMaP tiCMaPQ _; case/negP: ntCMaP.
-rewrite -subG1 -{}tiCMaPQ centY setICA subsetIidr /= -/Ma -/Q centsC.
-apply/commG1P/three_subgroup; apply/commG1P.
-  by rewrite commGC (commG1P _) ?sub1G ?subsetIr.
-apply: subset_trans (subsetIr Ma _); rewrite /= -symPR //.
-  rewrite commg_subl normsI //; last by rewrite norms_cent // cents_norm.
-  by rewrite (subset_trans sSM) ?gFnorm.
-apply: contraR aM'q => not_cRCaP; apply: pnatPpi (pgroupS sSMz _) piSq.
-by rewrite (negPf not_cRCaP) pcore_pgroup.
-Qed.
-
-(* This is B & G, Theorem 13.5. *)
-Theorem tau1_primact_Msigma E1 : \tau1(M).-Hall(E) E1 -> semiprime M`_\sigma E1.
-Proof.
-move=> hallE1 x /setD1P[]; rewrite -cycle_eq1 -cycle_subG => ntX sXE1.
-rewrite -cent_cycle; have [sE1E t1E1 _] := and3P hallE1.
-have [_ [E3 hallE3]] := ex_tau13_compl hallE.
-have{hallE3} [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3.
-have [_ _ [cycE1 _] _ _ {E2 E3 complEi}] := sigma_compl_context maxM complEi.
-apply/eqP; rewrite eqEsubset andbC setIS ?centS //= subsetI subsetIl /=.
-have [p _ rX] := rank_witness <[x]>; rewrite -rank_gt0 {}rX in ntX.
-have t1p: p \in \tau1(M) by rewrite (pnatPpi t1E1) // (piSg sXE1) -?p_rank_gt0.
-have{ntX} [P EpP] := p_rank_geP ntX; have{EpP} [sPX abelP dimP] := pnElemP EpP.
-have{sXE1} sPE1 := subset_trans sPX sXE1.
-have{dimP} EpP: P \in 'E_p^1(E) by rewrite !inE abelP dimP (subset_trans sPE1).
-apply: {x sPX abelP} subset_trans (setIS _ (centS sPX)) _; rewrite centsC.
-rewrite -(Sylow_gen E1) gen_subG; apply/bigcupsP=> S; case/SylowP=> r _ sylS.
-have [[sSE1 rS _] [-> | ntS]] := (and3P sylS, eqsVneq S 1); first exact: sub1G.
-have [cycS sSE] := (cyclicS sSE1 cycE1, subset_trans sSE1 sE1E).
-have /p_rank_geP[R ErR]: 0 < 'r_r(S) by rewrite -rank_pgroup ?rank_gt0.
-have{ErR} [sRS abelR dimR] := pnElemP ErR; have sRE1 := subset_trans sRS sSE1.
-have{abelR dimR} ErR: R \in 'E_r^1('C_E(P)).
-  rewrite !inE abelR dimR (subset_trans sRE1) // subsetI sE1E.
-  by rewrite sub_abelian_cent ?cyclic_abelian.
-rewrite centsC (subset_trans (cent_tau1Elem_Msigma t1p EpP ErR)) //.
-have [y defR]: exists y, R :=: <[y]> by apply/cyclicP; apply: cyclicS cycS.
-have sylS_E: r.-Sylow(E) S.
-  apply: subHall_Sylow hallE1 (pnatPpi t1E1 _) (sylS).
-  by rewrite -p_rank_gt0 -(rank_Sylow sylS) rank_gt0.
-rewrite defR cent_cycle (cyclic_primact_Msigma sylS_E cycS) ?subsetIr //.
-by rewrite !inE -cycle_subG -cycle_eq1 -defR (nt_pnElem ErR).
-Qed.
-
-(* This is B & G, Lemma 13.6. *)
-(* The wording at the top of the proof is misleading: it should say: by       *)
-(* Corollary 12.14, it suffices to show that we can't have both q \in beta(M) *)
-(* and X \notsubset M_sigma^(1). Also, the reference to 12.13 should be 12.19 *)
-(* or 10.9 (we've used 12.19 here).                                           *)
-Lemma cent_cent_Msigma_tau1_uniq E1 P q X (Ms := M`_\sigma) :
-    \tau1(M).-Hall(E) E1 -> P \subset E1 -> P :!=: 1 ->
-     X \in 'E_q^1('C_Ms(P)) ->
- 'M('C(X)) = [set M] /\ (forall S, q.-Sylow(Ms) S -> 'M(S) = [set M]).
-Proof.
-move=> hallE1 sPE1 ntP EqX; have [sE1E t1E1 _] := and3P hallE1.
-rewrite (cent_semiprime (tau1_primact_Msigma hallE1)) //= -/Ms in EqX.
-have{P ntP sPE1} ntE1 := subG1_contra sPE1 ntP.
-have /andP[sMsM nMsM]: Ms <| M := pcore_normal _ M.
-have coMsE: coprime #|Ms| #|E| := coprime_sigma_compl hallE.
-have [solMs nMsE] := (solvableS sMsM (mmax_sol maxM), subset_trans sEM nMsM).
-apply: cent_der_sigma_uniq => //.
-  by move: EqX; rewrite -(setIidPr sMsM) -setIA pnElemI => /setIP[].
-have{EqX} [[sXcMsE1 abelX _] ntX] := (pnElemP EqX, nt_pnElem EqX isT).
-apply: contraR ntX => /norP[b'q not_sXMs']; rewrite -subG1.
-have [S sylS nSE] := coprime_Hall_exists q nMsE coMsE solMs.
-have{abelX} [[sSMs qS _] [qX _]] := (and3P sylS, andP abelX).
-have sScMsE': S \subset 'C_Ms(E^`(1)).
-  have [H hallH cHE'] := der_compl_cent_beta' maxM hallE.
-  have [Q sylQ] := Sylow_exists q H; have [sQH qQ _] := and3P sylQ.
-  have{cHE' sQH} cQE' := centsS sQH cHE'; have sE'E := der_sub 1 E.
-  have [nMsE' coMsE'] := (coprimegS sE'E coMsE, subset_trans sE'E nMsE).
-  have{H hallH sylQ} sylQ := subHall_Sylow hallH b'q sylQ.
-  have nSE' := subset_trans sE'E nSE; have nQE' := cents_norm cQE'.
-  have [x cE'x ->] := coprime_Hall_trans coMsE' nMsE' solMs sylS nSE' sylQ nQE'.
-  by rewrite conj_subG // subsetI (pHall_sub sylQ) centsC.
-without loss{qX} sXS: X sXcMsE1 not_sXMs' / X \subset S.
-  have [nMsE1 coMsE1 IH] := (subset_trans sE1E nMsE, coprimegS sE1E coMsE).
-  have [nSE1 [sXMs cE1X]] := (subset_trans sE1E nSE, subsetIP sXcMsE1).
-  have [|Q [sylQ nQE1 sXQ]] := coprime_Hall_subset nMsE1 coMsE1 solMs sXMs qX.
-    by rewrite cents_norm // centsC.
-  have [//|x cE1x defS] := coprime_Hall_trans nMsE1 _ solMs sylS nSE1 sylQ nQE1.
-  have Ms_x: x \in Ms by case/setIP: cE1x.
-  rewrite -(conjs1g x^-1) -sub_conjg IH //; last by rewrite defS conjSg.
-    by rewrite -(conjGid cE1x) conjSg.
-  by rewrite -(normsP (der_norm 1 _) x) ?conjSg.
-have [sXMs cE1X] := subsetIP sXcMsE1.
-have [_ [E3 hallE3]] := ex_tau13_compl hallE.
-have{hallE3} [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3.
-have{not_sXMs' E3 complEi} ntE2: E2 :!=: 1.
-  apply: contraNneq not_sXMs' => E2_1.
-  have [[sE3E' _] _ _ [defE _] _] := sigma_compl_context maxM complEi.
-  have [sCMsE_Ms' _ _] := sigma_compl_embedding maxM hallE.
-  have{defE} [_ defE _ _] := sdprodP defE; rewrite E2_1 sdprod1g in defE.
-  rewrite (subset_trans _ sCMsE_Ms') // -defE centM setIA subsetI.
-  by rewrite (subset_trans (subset_trans sXS sScMsE')) ?setIS ?centS.
-have{ntE2 E2 hallE2} [p p_pr t2p]: exists2 p, prime p & p \in \tau2(M).
-  have [[p p_pr rE2] [_ t2E2 _]] := (rank_witness E2, and3P hallE2).
-  by exists p; rewrite ?(pnatPpi t2E2) // -p_rank_gt0 -rE2 rank_gt0.
-have [A Ep2A Ep2A_M] := ex_tau2Elem hallE t2p.
-have [_ _ tiCMsA _ _] := tau2_context maxM t2p Ep2A_M.
-have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2p Ep2A.
-have [sAE abelA _] := pnElemP Ep2A; have [pA cAA _] := and3P abelA.
-have cCAE1_X: X \subset 'C('C_A(E1)).
-  rewrite centsC; apply/subsetP=> y; case/setIP=> Ay cE1y.
-  have [-> | nty] := eqVneq y 1; first exact: group1.
-  have oY: #[y] = p := abelem_order_p abelA Ay nty.
-  have [r _ rE1] := rank_witness E1.
-  have{rE1} rE1: 'r_r(E1) > 0 by rewrite -rE1 rank_gt0.
-  have [R ErR] := p_rank_geP rE1; have{ErR} [sRE1 abelR dimR] := pnElemP ErR.
-  have t1r: r \in \tau1(M) by rewrite (pnatPpi t1E1) -?p_rank_gt0.
-  have ErR: R \in 'E_r^1(E) by rewrite !inE abelR dimR (subset_trans sRE1).
-  have EpY: <[y]>%G \in 'E_p^1('C_E(R)).
-    rewrite p1ElemE // !inE -oY eqxx subsetI (centsS sRE1) cycle_subG //=.
-    by rewrite (subsetP sAE).
-  rewrite -sub_cent1 -cent_cycle (subset_trans sXcMsE1) //.
-  apply: subset_trans (setIS _ (centS sRE1)) _.
-  rewrite -subsetIidl setIAC subsetI subsetIr andbT.
-  exact: cent_tau1Elem_Msigma t1r ErR EpY.
-have nAE1 := subset_trans sE1E (normal_norm nsAE).
-have coAE1: coprime #|A| #|E1|.
-  by apply: pnat_coprime pA (pi_p'group t1E1 (contraL _ t2p)); apply: tau2'1.
-rewrite -tiCMsA -(coprime_cent_prod nAE1 coAE1) ?abelian_sol // centM setIA.
-rewrite subsetI cCAE1_X (subset_trans (subset_trans sXS sScMsE')) ?setIS //.
-by rewrite centS ?commgSS.
-Qed.
-
-End OneComplement.
-
-(* This is B & G, Lemma 13.7. *)
-(* We've had to plug a gap in this proof: on p. 100, l. 6-7 it is asserted    *)
-(* the conclusion (E1 * E3 acts in a prime manner on M_sigma) follows from    *)
-(* the fact that E1 and E3 have coprime orders and act in a prime manner with *)
-(* the same set of fixed points. This seems to imply the following argument:  *)
-(*   For any x \in M_sigma,                                                   *)
-(*       C_(E1 * E3)[x] = C_E1[x] * C_E3[x] is either E1 * E3 or 1,           *)
-(*   i.e., E1 * E3 acts in a prime manner on M_sigma.                         *)
-(* This is improper because the distributivity of centralisers over coprime   *)
-(* products only hold under normality conditions that do not hold in this     *)
-(* instance. The correct argument, which involves using the prime action      *)
-(* assumption a second time, only relies on the fact that E1 and E3 are Hall  *)
-(* subgroups of the group E1 * E3. The fact that E3 <| E (Lemma 12.1(a)),     *)
-(* implicitly needed to justify that E1 * E3 is a group, can also be used to  *)
-(* simplify the argument, and we do so.                                       *)
-Lemma tau13_primact_Msigma M E E1 E2 E3 :
-    M \in 'M -> sigma_complement M E E1 E2 E3 -> ~ semiregular E3 E1 ->
-  semiprime M`_\sigma (E3 <*> E1).
-Proof.
-move=> maxM complEi not_regE13; set Ms := M`_\sigma.
-have [hallE hallE1 hallE2 hallE3 _] := complEi.
-have [[sE1E t1E1 _] [sE3E t3E3 _]] := (and3P hallE1, and3P hallE3).
-have [[sEM _ _] [_ t2E2 _]] := (and3P hallE, and3P hallE2).
-have [[_ nsE3E] _ [_ cycE3] [defE _] tiE3cE]:= sigma_compl_context maxM complEi.
-have [[_ nE3E] [sMsM nMsM]] := (andP nsE3E, andP (pcore_normal _ M : Ms <| M)).
-have [P]: exists2 P, P \in 'E^1(E1) & 'C_E3(P) != 1.
-  apply/exists_inP; rewrite -negb_forall_in; apply/forall_inP=> regE13.
-  apply: not_regE13 => x /setD1P[]; rewrite -cycle_subG -cycle_eq1 -rank_gt0.
-  case/rank_geP=> P E1xP sXE1; apply/trivgP; move: E1xP.
-  rewrite /= -(setIidPr sXE1) nElemI -setIdE => /setIdP[E1_P sPX].
-  by rewrite -(eqP (regE13 P E1_P)) -cent_cycle setIS ?centS.
-rewrite -{1}(setIidPr sE1E) nElemI -setIdE => /setIdP[/nElemP[p EpP] sPE1].
-rewrite -{1}(setIidPl sE3E) -setIA setIC -rank_gt0 => /rank_geP[R].
-rewrite nElemI -setIdE => /setIdP[/nElemP[r ErR] sRE3].
-have t1p: p \in \tau1(M).
-  rewrite (pnatPpi (pgroupS sPE1 t1E1)) //= (card_p1Elem EpP).
-  by rewrite pi_of_prime ?inE ?(pnElem_prime EpP) //.
-have prE1 := tau1_primact_Msigma maxM hallE hallE1.
-have prE3 := tau3_primact_Msigma maxM hallE hallE3.
-have sCsPR: 'C_Ms(P) \subset 'C_Ms(R) by apply: cent_tau1Elem_Msigma EpP ErR.
-have [eqCsPR | ltCsPR] := eqVproper sCsPR.
-  move=> x; case/setD1P; rewrite -cycle_eq1 -cycle_subG => ntX sXE31.
-  apply/eqP; rewrite -cent_cycle eqEsubset andbC setIS ?centS //=.
-  have eqCsE13: 'C_Ms(E1) = 'C_Ms(E3).
-    rewrite -(cent_semiprime prE1 sPE1) ?(nt_pnElem EpP) //.
-    by rewrite -(cent_semiprime prE3 sRE3) ?(nt_pnElem ErR).
-  rewrite centY setICA eqCsE13 -setICA setIid.
-  have sE31E: E3 <*> E1 \subset E by apply/joing_subP.
-  have nE3E1 := subset_trans sE1E nE3E.
-  pose y := x.`_\tau1(M); have sYX: <[y]> \subset <[x]> := cycleX x _.
-  have sXE := subset_trans sXE31 sE31E; have sYE := subset_trans sYX sXE.
-  have [t1'x | not_t1'x] := boolP (\tau1(M)^'.-elt x).
-    rewrite (cent_semiprime prE3 _ ntX) // (sub_normal_Hall hallE3) //.
-    apply: pnat_dvd t3E3; rewrite -(Gauss_dvdr _ (p'nat_coprime t1'x t1E1)).
-    by rewrite mulnC (dvdn_trans _ (dvdn_cardMg _ _)) -?norm_joinEr ?cardSg.
-  have{not_t1'x} ntY: #[y] != 1%N by rewrite order_constt partn_eq1.
-  apply: subset_trans (setIS _ (centS sYX)) _.
-  have [solE nMsE] := (sigma_compl_sol hallE, subset_trans sEM nMsM).
-  have [u Eu sYuE1] := Hall_Jsub solE hallE1 sYE (p_elt_constt _ _).
-  rewrite -(conjSg _ _ u) !conjIg -!centJ (normsP nMsE) ?(normsP nE3E) //=.
-  by rewrite -eqCsE13 (cent_semiprime prE1 sYuE1) // trivg_card1 cardJg.
-have ntCsR: 'C_Ms(R) != 1.
-  by rewrite -proper1G (sub_proper_trans _ ltCsPR) ?sub1G.
-have ntR: R :!=: 1 by rewrite (nt_pnElem ErR).
-have [cEPR abelR dimR] := pnElemP ErR; have [rR _ _] := and3P abelR.
-have{cEPR} [sRE cPR] := subsetIP cEPR; have sRM := subset_trans sRE sEM.
-have E2_1: E2 :=: 1.
-  have [x defR] := cyclicP (cyclicS sRE3 cycE3).
-  apply: contraNeq ntCsR; rewrite -rank_gt0; have [q _ ->] := rank_witness E2.
-  rewrite p_rank_gt0 defR cent_cycle. move/(pnatPpi t2E2) => t2q.
-  have [A Eq2A _] := ex_tau2Elem hallE t2q.
-  have [-> //] := tau2_regular maxM complEi t2q Eq2A.
-  by rewrite !inE -cycle_subG -cycle_eq1 -defR sRE3 (nt_pnElem ErR).
-have nRE: E \subset 'N(R) by rewrite (char_norm_trans _ nE3E) ?sub_cyclic_char.
-have [H maxNH] := mmax_exists (mFT_norm_proper ntR (mFT_pgroup_proper rR)).
-have [maxH sNH] := setIdP maxNH; have sEH := subset_trans nRE sNH.
-have ntCsR_P: [~: 'C_Ms(R), P] != 1.
-  rewrite (sameP eqP commG1P); apply: contra (proper_subn ltCsPR).
-  by rewrite subsetI subsetIl.
-have sCsR_MsH: 'C_Ms(R) \subset Ms :&: H.
-  exact: setIS Ms (subset_trans (cent_sub R) sNH).
-have ntMsH_P: [~: Ms :&: H, P] != 1 by rewrite (subG1_contra _ ntCsR_P) ?commSg.
-have tiE1cMsH: 'C_E1(Ms :&: H) = 1.
-  apply: contraNeq (proper_subn ltCsPR) => ntCE1MsH.
-  rewrite (cent_semiprime prE1 sPE1) ?(nt_pnElem EpP) //.
-  rewrite -(cent_semiprime prE1 (subsetIl _ _) ntCE1MsH) /=.
-  by rewrite subsetI subsetIl centsC subIset // orbC centS.
-have t3r: r \in \tau3(M).
-  by rewrite (pnatPpi t3E3) ?(piSg sRE3) // -p_rank_gt0 p_rank_abelem ?dimR.
-have t13r: (r \in \tau1(M)) || (r \in \tau3(M)) by rewrite t3r orbT.
-have [sE1H sRH] := (subset_trans sE1E sEH, subset_trans sRE sEH).
-have [_ ct1H'R [|sHr _]] := cent_norm_tau13_mmax maxM hallE t13r sRM rR maxNH.
-  rewrite (subG1_contra _ ntMsH_P) // commgS // (subset_trans sPE1) //.
-  by rewrite subsetI (subset_trans sE1E).
-have t1H_E1: \tau1(H).-group E1.
-  apply/pgroupP=> q q_pr /Cauchy[] // x E1x ox.
-  apply: contraLR (prime_gt1 q_pr) => t1H'q; rewrite -ox cardG_gt1 negbK.
-  rewrite -subG1 -tiE1cMsH subsetI cycle_subG E1x /= ct1H'R //.
-    by rewrite (setIidPl sEH) cycle_subG (subsetP sE1E).
-  by rewrite /pgroup -orderE ox pnatE.
-have sH'_E1: \sigma(H)^'.-group E1 by apply: sub_pgroup t1H_E1 => q /andP[].
-have [F hallF sE1F] := Hall_superset (mmax_sol maxH) sE1H sH'_E1.
-have [F1 hallF1 sE1F1] := Hall_superset (sigma_compl_sol hallF) sE1F t1H_E1.
-have{sHr} sRHs: R \subset H`_\sigma.
-  by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) ?(pi_pgroup rR).
-have cRE1: E1 \subset 'C(R).
-  rewrite centsC (centsS sE1F1) // -subsetIidl subsetI subxx -sRHs -subsetI.
-  have prF1 := tau1_primact_Msigma maxH hallF hallF1.
-  rewrite -(cent_semiprime prF1 (subset_trans sPE1 sE1F1)); last first.
-    exact: nt_pnElem EpP _.
-  by rewrite subsetI sRHs.
-case/negP: ntR; rewrite -subG1 -tiE3cE subsetI sRE3 centsC -(sdprodW defE).
-by rewrite E2_1 sdprod1g mul_subG // sub_abelian_cent ?cyclic_abelian.
-Qed.
-
-(* This is B & G, Lemma 13.8. *)
-(* We had to plug a significant hole in the proof text: in the sixth          *)
-(* paragraph of the proof, it is asserted that because M = N_M(Q)M_alpha and  *)
-(* r is in pi(C_M(P)), P centralises some non-trivial r-subgroup of N_M(Q).   *)
-(* This does not seem to follow directly, even taking into account that r is  *)
-(* not in alpha(M): while it is true that N_M(Q) contains a Sylow r-subgroup  *)
-(* of M, this subgroup does not need to contain an r-group centralized by P.  *)
-(* We can only establish the required result by making use of the fact that M *)
-(* has a normal p-complement K (because p is in tau_1(M)), as then N_K(Q)     *)
-(* will contain a p-invariant Sylow r-subgroup S of K and M (coprime action)  *)
-(* and then any r-subgroup of M centralised by P will be in K, and hence      *)
-(* conjugate in C_K(P) to a subgroup of S (coprime action again).             *)
-Lemma tau1_mmaxI_asymmetry M Mstar p P q Q q_star Qstar :
-  (*1*) [/\ M \in 'M, Mstar \in 'M & gval Mstar \notin M :^: G] ->
-  (*2*) [/\ p \in \tau1(M), p \in \tau1(Mstar) & P \in 'E_p^1(M :&: Mstar)] ->
-  (*3*) [/\ q.-Sylow(M :&: Mstar) Q, q_star.-Sylow(M :&: Mstar) Qstar,
-            P \subset 'N(Q) & P \subset 'N(Qstar)] ->
-  (*4*) 'C_Q(P) = 1 /\ 'C_Qstar(P) = 1 ->
-  (*5*) 'N(Q) \subset Mstar /\ 'N(Qstar) \subset M ->
-  False.
-Proof.
-move: Mstar q_star Qstar => L u U. (* Abbreviate Mstar by L, Qstar by U. *)
-move=> [maxM maxL notMGL] [t1Mp t1Lp EpP] [sylQ sylU nQP nUP].
-move=> [regPQ regPU] [sNQL sNUM]; rewrite setIC in sylU. (* for symmetry *)
-have notLGM: gval M \notin L :^: G by rewrite orbit_sym. (* for symmetry *)
-have{EpP} [ntP [sPML abelP dimP]] := (nt_pnElem EpP isT, pnElemP EpP).
-have{sPML} [[sPM sPL] [pP _ _]] := (subsetIP sPML, and3P abelP).
-have solCP: solvable 'C(P) by rewrite mFT_sol ?mFT_cent_proper.
-pose Qprops M q Q := [&& q.-Sylow(M) Q, q != p, q \notin \beta(M),
-                          'C_(M`_\beta)(P) != 1 & 'C_(M`_\beta)(P <*> Q) == 1].
-have{sylQ sylU} [hypQ hypU]: Qprops M q Q /\ Qprops L u U.
-  apply/andP; apply/nandP=> not_hypQ.
-  without loss{not_hypQ}: L u U M q Q maxM maxL notMGL notLGM t1Mp t1Lp sPM sPL
-                  sylQ sylU nQP nUP regPQ regPU sNQL sNUM / ~~ Qprops M q Q.
-  - by move=> IH; case: not_hypQ; [apply: (IH L u U) | apply: (IH M q Q)].
-  case/and5P; have [_ qQ _] := and3P sylQ.
-  have{sylQ} sylQ: q.-Sylow(M) Q.
-    by rewrite -Sylow_subnorm -(setIidPr sNQL) setIA Sylow_subnorm.
-  have ntQ: Q :!=: 1.
-    by apply: contraTneq sNQL => ->; rewrite norm1 proper_subn ?mmax_proper.
-  have p'q: q != p.
-    apply: contraNneq ntQ => def_q; rewrite (trivg_center_pgroup qQ) //.
-    apply/trivgP; rewrite -regPQ setIS // centS //.
-    by rewrite (norm_sub_max_pgroup (Hall_max sylQ)) ?def_q.
-  have EpP: P \in 'E_p^1(M) by apply/pnElemP.
-  have [|_ [// | abM]] := cent_Malpha_reg_tau1 maxM t1Mp p'q EpP ntQ nQP regPQ.
-    apply: contraNneq notMGL => uniqNQ.
-    by rewrite (eq_uniq_mmax uniqNQ) ?orbit_refl.
-  by rewrite joingC /alpha_core abM !(eq_pcore _ abM) => _ -> -> ->.
-have bML_CMbP: forall M L, [predU \beta(M) & \beta(L)].-group 'C_(M`_\beta)(P).
-  move=> ? ?; apply: pgroupS (subsetIl _ _) (sub_pgroup _ (pcore_pgroup _ _)).
-  by move=> ?; rewrite !inE => ->.
-have [H hallH sCMbP_H] := Hall_superset solCP (subsetIr _ _) (bML_CMbP M L).
-have [[s _ rFH] [cPH bH _]] := (rank_witness 'F(H), and3P hallH).
-have{sCMbP_H rFH cPH} piFHs: s \in \pi('F(H)).
-  rewrite -p_rank_gt0 -rFH rank_gt0 (trivg_Fitting (solvableS cPH solCP)).
-  by rewrite (subG1_contra sCMbP_H) //; case/and5P: hypQ.
-without loss{bH} bMs: L u U M q Q maxM maxL notMGL notLGM t1Mp t1Lp sPM sPL
-               nQP nUP regPQ regPU sNQL sNUM hypQ hypU hallH / s \in \beta(M).
-- move=> IH; have:= pnatPpi bH (piSg (Fitting_sub H) piFHs).
-  case/orP; [apply: IH hypQ hypU hallH | apply: IH hypU hypQ _] => //.
-  by apply: etrans (eq_pHall _ _ _) hallH => ?; apply: orbC.
-without loss{bML_CMbP} sCMbP_H: H hallH piFHs / 'C_(M`_\beta)(P) \subset H.
-  have [x cPx sCMbP_Hx] := Hall_subJ solCP hallH (subsetIr _ _) (bML_CMbP M L).
-  by move=> IH; apply: IH sCMbP_Hx; rewrite ?pHallJ //= FittingJ cardJg.
-pose X := 'O_s(H); have sylX := nilpotent_pcore_Hall s (Fitting_nil H).
-have{piFHs sylX} ntX: X != 1.
-  by rewrite -rank_gt0 /= -p_core_Fitting (rank_Sylow sylX) p_rank_gt0.
-have [[cPH bH _] [sXH nXH]] := (and3P hallH, andP (pcore_normal s H : X <| H)).
-have [cPX sX] := (subset_trans sXH cPH, pcore_pgroup s H : s.-group X).
-have{hypQ} [sylQ p'q bM'q ntCMbP] := and5P hypQ; apply: negP.
-apply: subG1_contra (ntX); rewrite /= centY !subsetI (subset_trans _ cPH) //=.
-have nsMbM : M`_\beta <| M := pcore_normal _ M; have [sMbM nMbM] := andP nsMbM.
-have hallMb := Mbeta_Hall maxM; have [_ bMb _] := and3P hallMb.
-have{ntX} sHM: H \subset M.
-  have [g sXMg]: exists g, X \subset M :^ g.
-    have [S sylS] := Sylow_exists s M`_\beta; have [sSMb _ _] := and3P sylS.
-    have sylS_G := subHall_Sylow (Mbeta_Hall_G maxM) bMs sylS.
-    have [g _ sXSg] := Sylow_subJ sylS_G (subsetT X) sX.
-    by exists g; rewrite (subset_trans sXSg) // conjSg (subset_trans sSMb).
-  have [t _ rFC] := rank_witness 'F('C_(M`_\beta)(P)).
-  pose Y := 'O_t('C_(M`_\beta)(P)).
-  have [sYC tY] := (pcore_sub t _ : Y \subset _, pcore_pgroup t _ : t.-group Y).
-  have sYMb := subset_trans sYC (subsetIl _ _); have bMY := pgroupS sYMb bMb.
-  have{rFC} ntY: Y != 1.
-    rewrite -rank_gt0 /= -p_core_Fitting.
-    rewrite (rank_Sylow (nilpotent_pcore_Hall t (Fitting_nil _))) -rFC.
-    by rewrite rank_gt0 (trivg_Fitting (solvableS (subsetIr _ _) solCP)).
-  have bMt: t \in \beta(M).
-    by rewrite (pnatPpi bMY) // -p_rank_gt0 -rank_pgroup ?rank_gt0.
-  have sHMg: H \subset M :^ g.
-    rewrite (subset_trans nXH) // beta_norm_sub_mmax ?mmaxJ // /psubgroup sXMg.
-    by rewrite (pi_pgroup sX) 1?betaJ.
-  have sYMg: Y \subset M :^ g := subset_trans (subset_trans sYC sCMbP_H) sHMg.
-  have sNY_M: 'N(Y) \subset M.
-    by rewrite beta_norm_sub_mmax // /psubgroup (subset_trans sYMb).
-  have [_ trCY _] := sigma_group_trans maxM (beta_sub_sigma maxM bMt) tY.
-  have [|| h cYh /= defMg] := (atransP2 trCY) M (M :^ g).
-  - by rewrite inE orbit_refl (subset_trans (normG _) sNY_M).
-  - by rewrite inE mem_orbit ?in_setT.
-  by rewrite defMg conjGid // (subsetP sNY_M) ?(subsetP (cent_sub _)) in sHMg.
-have sXMb: X \subset M`_\beta.
-  by rewrite (sub_Hall_pcore hallMb) ?(subset_trans sXH sHM) ?(pi_pgroup sX).
-rewrite sXMb (sameP commG1P eqP) /= -/X -subG1.
-have [sQL [sQM qQ _]] := (subset_trans (normG Q) sNQL, and3P sylQ).
-have nsLbL : L`_\beta <| L := pcore_normal _ L; have [sLbL nLbL] := andP nsLbL.
-have nLbQ := subset_trans sQL nLbL.
-have [<- ti_aLsM _] := sigma_disjoint maxL maxM notLGM.
-rewrite subsetI (subset_trans _ (Mbeta_sub_Msigma maxM)) ?andbT; last first.
-  by rewrite (subset_trans (commgSS sXMb sQM)) // commg_subl nMbM.
-have defQ: [~: Q, P] = Q.
-  rewrite -{2}(coprime_cent_prod nQP) ?(pgroup_sol qQ) ?regPQ ?mulg1 //.
-  by rewrite (p'nat_coprime (pi_pnat qQ _) pP).
-suffices sXL: X \subset L.
-  apply: subset_trans (Mbeta_sub_Malpha L).
-  rewrite -quotient_sub1 ?comm_subG  ?quotientR ?(subset_trans _ nLbL) //.
-  have <-: (M`_\beta :&: L) / L`_\beta :&: 'O_q(L^`(1) / L`_\beta) = 1.
-    rewrite coprime_TIg // coprime_morphl // (coprimeSg (subsetIl _ _)) //.
-    exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat (pcore_pgroup _ _) _).
-  rewrite commg_subI // subsetI.
-    rewrite quotientS /=; last by rewrite subsetI sXMb.
-    by rewrite quotient_der ?gFnorm_trans ?normsG ?quotientS.
-  rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ (Mbeta_quo_nil _))) //.
-    rewrite quotient_pgroup ?quotient_norms //.
-    by rewrite normsI ?(subset_trans sQM nMbM) ?normsG.
-  by rewrite quotientS // -defQ commgSS // (subset_trans nQP).
-have{hypU} [r bLr piHr]: exists2 r, r \in \beta(L) & r \in \pi(H).
-  have [_ _ _] := and5P hypU; rewrite -rank_gt0.
-  have [r _ ->] := rank_witness 'C_(L`_\beta)(P); rewrite p_rank_gt0 => piCr _.
-  have [piLb_r piCPr] := (piSg (subsetIl _ _) piCr, piSg (subsetIr _ _) piCr).
-  have bLr: r \in \beta(L) := pnatPpi (pcore_pgroup _ L) piLb_r.
-  exists r; rewrite //= (card_Hall hallH) pi_of_part // inE /= piCPr.
-  by rewrite inE /= bLr orbT.
-have sM'r: r \notin \sigma(M).
-  by apply: contraFN (ti_aLsM r) => sMr; rewrite inE /= beta_sub_alpha.
-have defM: M`_\beta * 'N_M(Q) = M.
-  have nMbQ := subset_trans sQM nMbM.
-  have nsMbQ_M: M`_\beta <*> Q <| M.
-    rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //.
-    suffices ->: Q / M`_\beta = 'O_q(M^`(1) / M`_\beta).
-      by rewrite quotient_der ?nMbM ?gFnormal_trans.
-    apply: nilpotent_Hall_pcore; first exact: Mbeta_quo_nil.
-    rewrite quotient_pHall // (pHall_subl _ _ sylQ) ?gFsub //.
-    by rewrite -defQ commgSS // (subset_trans nUP).
-  have sylQ_MbQ := pHall_subl (joing_subr _ Q) (normal_sub nsMbQ_M) sylQ.
-  rewrite -{3}(Frattini_arg nsMbQ_M sylQ_MbQ) /= norm_joinEr // -mulgA.
-  by congr (_ * _); rewrite mulSGid // subsetI sQM normG.
-have [[sM'p _ not_pM'] [sL'p _]] := (and3P t1Mp, andP t1Lp).
-have{not_pM'} [R ErR nQR]: exists2 R, R \in 'E_r^1('C_M(P)) & R \subset 'N(Q).
-  have p'r: r \in p^' by apply: contraNneq sL'p => <-; apply: beta_sub_sigma.
-  have p'M': p^'.-group M^`(1).
-    by rewrite p'groupEpi mem_primes (negPf not_pM') !andbF.
-  pose K := 'O_p^'(M); have [sKM nKM] := andP (pcore_normal _ M : K <| M).
-  have hallK: p^'.-Hall(M) K.
-    rewrite -(pquotient_pHall _ (der_normal 1 M)) ?quotient_pgroup //.
-      rewrite -pquotient_pcore ?der_normal // nilpotent_pcore_Hall //.
-      by rewrite abelian_nil ?der_abelian.
-    by rewrite (normalS _ sKM) ?pcore_max ?der_normal.
-  have sMbK: M`_\beta \subset K.
-    by rewrite (subset_trans (Mbeta_der1 maxM)) // pcore_max ?der_normal.
-  have coKP: coprime #|K| #|P| := p'nat_coprime (pcore_pgroup _ M) pP.
-  have [solK sNK] := (solvableS sKM (mmax_sol maxM), subsetIl K 'N(Q)).
-  have [nKP coNP] := (subset_trans sPM nKM, coprimeSg sNK coKP).
-  have nNP: P \subset 'N('N_K(Q)) by rewrite normsI // norms_norm.
-  have [S sylS nSP] := coprime_Hall_exists r nNP coNP (solvableS sNK solK).
-  have /subsetIP[sSK nQS]: S \subset 'N_K(Q) := pHall_sub sylS.
-  have sylS_K: r.-Sylow(K) S.
-    rewrite pHallE sSK /= -/K -(setIidPr sKM) -defM -group_modl // setIAC.
-    rewrite (setIidPr sKM) -LagrangeMr partnM // -(card_Hall sylS).
-    rewrite part_p'nat ?mul1n 1?(pnat_dvd (dvdn_indexg _ _)) //.
-    by apply: (pi_p'nat bMb); apply: contra sM'r; apply: beta_sub_sigma.
-  have rC: 'r_r('C_M(P)) > 0 by rewrite p_rank_gt0 (piSg _ piHr) // subsetI sHM.
-  have{rC} [R ErR] := p_rank_geP rC; have [sRcMP abelR _] := pnElemP ErR.
-  have{sRcMP abelR} [[sRM cPR] [rR _]] := (subsetIP sRcMP, andP abelR).
-  have nRP: P \subset 'N(R) by rewrite cents_norm 1?centsC.
-  have sRK: R \subset K by rewrite sub_Hall_pcore ?(pi_pgroup rR).
-  have [T [sylT nTP sRT]] := coprime_Hall_subset nKP coKP solK sRK rR nRP.
-  have [x cKPx defS] := coprime_Hall_trans nKP coKP solK sylS_K nSP sylT nTP.
-  rewrite -(conjGid (subsetP (setSI _ sKM) x cKPx)).
-  by exists (R :^ x)%G; rewrite ?pnElemJ ?(subset_trans _ nQS) // defS conjSg.
-have [sRcMP abelR _] := pnElemP ErR; have ntR := nt_pnElem ErR isT.
-have{sRcMP abelR} [[sRM cPR] [rR _]] := (subsetIP sRcMP, andP abelR).
-have sNR_L: 'N(R) \subset L.
-  by rewrite beta_norm_sub_mmax /psubgroup ?(subset_trans nQR) ?(pi_pgroup rR).
-have sPR_M: P <*> R \subset M by rewrite join_subG (subset_trans nUP).
-have sM'_PR: \sigma(M)^'.-group (P <*> R).
-  by rewrite cent_joinEr // pgroupM (pi_pgroup rR) // (pi_pgroup pP).
-have [E hallE sPRE] := Hall_superset (mmax_sol maxM) sPR_M sM'_PR.
-have{sPRE} [sPE sRE] := joing_subP sPRE.
-have EpP: P \in 'E_p^1(E) by apply/pnElemP.
-have{ErR} ErR: R \in 'E_r^1('C_E(P)).
-  by rewrite -(setIidPr (pHall_sub hallE)) setIAC pnElemI inE ErR inE.
-apply: subset_trans (cents_norm (subset_trans _ (subsetIr M`_\sigma _))) sNR_L.
-apply: subset_trans (cent_tau1Elem_Msigma maxM hallE t1Mp EpP ErR).
-by rewrite subsetI cPX (subset_trans sXMb) ?Mbeta_sub_Msigma.
-Qed.
-
-(* This is B & G, Theorem 13.9. *)
-Theorem sigma_partition M Mstar :
-    M \in 'M -> Mstar \in 'M -> gval Mstar \notin M :^: G ->
-  [predI \sigma(M) & \sigma(Mstar)] =i pred0.
-Proof.
-move: Mstar => L maxM maxL notMGL q; apply/andP=> [[/= sMq sLq]].
-have [E hallE] := ex_sigma_compl maxM; have [sEM sM'E _] := and3P hallE.
-have [_ _ nMsE _] := sdprodP (sdprod_sigma maxM hallE).
-have coMsE: coprime #|M`_\sigma| #|E| := pnat_coprime (pcore_pgroup _ _) sM'E.
-have [|S sylS nSE] := coprime_Hall_exists q nMsE coMsE.
-  exact: solvableS (pcore_sub _ _) (mmax_sol maxM).
-have [sSMs qS _] := and3P sylS.
-have sylS_M := subHall_Sylow (Msigma_Hall maxM) sMq sylS.
-have ntS: S :!=: 1.
-  by rewrite -rank_gt0 (rank_Sylow sylS_M) p_rank_gt0 sigma_sub_pi.
-without loss sylS_L: L maxL sLq notMGL / q.-Sylow(L) S.
-  have sylS_G := sigma_Sylow_G maxM sMq sylS_M.
-  have [T sylT] := Sylow_exists q L; have sylT_G := sigma_Sylow_G maxL sLq sylT.
-  have [x Gx ->] := Sylow_trans sylT_G (sigma_Sylow_G maxM sMq sylS_M).
-  case/(_ (L :^ x)%G); rewrite ?mmaxJ ?sigmaJ ?pHallJ2 //.
-  by rewrite (orbit_transl _ (mem_orbit 'Js L Gx)).
-have [[sSL _] [[E1 hallE1] [E3 hallE3]]] := (andP sylS_L, ex_tau13_compl hallE).
-have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3.
-have E2_1: E2 :==: 1.
-  apply: contraR ntS; rewrite -rank_gt0; have [p _ ->] := rank_witness E2.
-  rewrite p_rank_gt0 => /(pnatPpi (pHall_pgroup hallE2))t2p.
-  have [A Ep2A _] := ex_tau2Elem hallE t2p.
-  have [_ _ _ ti_sM] := tau2_compl_context maxM hallE t2p Ep2A.
-  rewrite -subG1; have [<- _] := ti_sM L maxL notMGL; rewrite subsetI sSMs /=.
-  by rewrite (sub_Hall_pcore (Msigma_Hall maxL) sSL) (pi_pgroup qS).
-have: E1 :!=: 1 by have [_ -> //] := sigma_compl_context maxM complEi.
-rewrite -rank_gt0; have [p _ ->] := rank_witness E1; case/p_rank_geP=> P EpP.
-have [[sPE1 abelP dimP] [sE1E t1E1 _]] := (pnElemP EpP, and3P hallE1).
-have ntP: P :!=: 1 by rewrite (nt_pnElem EpP).
-have piPp: p \in \pi(P) by rewrite -p_rank_gt0 ?p_rank_abelem ?dimP.
-have t1Mp: p \in \tau1(M) by rewrite (pnatPpi _ (piSg sPE1 _)).
-have sPE := subset_trans sPE1 sE1E; have sPM := subset_trans sPE sEM.
-have [sNM sNL] := (norm_sigma_Sylow sMq sylS_M, norm_sigma_Sylow sLq sylS_L).
-have nSP := subset_trans sPE nSE; have sPL := subset_trans nSP sNL.
-have regPS: 'C_S(P) = 1.
-  apply: contraNeq (contra_orbit _ _ notMGL); rewrite -rank_gt0.
-  rewrite (rank_pgroup (pgroupS _ qS)) ?subsetIl //; case/p_rank_geP=> Q /=.
-  rewrite -(setIidPr sSMs) setIAC pnElemI; case/setIdP=> EqQ _.
-  have [_ uniqSq] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sPE1 ntP EqQ.
-  by rewrite (eq_uniq_mmax (uniqSq S sylS) maxL sSL).
-have t1Lp: p \in \tau1(L).
-  have not_cMsL_P: ~~ (P \subset 'C(M`_\sigma :&: L)).
-    apply: contra ntS => cMsL_P; rewrite -subG1 -regPS subsetIidl centsC.
-    by rewrite (subset_trans cMsL_P) ?centS // subsetI sSMs.
-  apply: contraR (not_cMsL_P) => t1L'p.
-  have [piEp piLp] := (piSg sPE piPp, piSg sPL piPp).
-  have [] := Msigma_setI_mmax_central maxM hallE maxL piEp piLp t1L'p _ notMGL.
-    apply: contraNneq not_cMsL_P; move/commG1P; rewrite centsC.
-    by apply: subset_trans; rewrite subsetI sPM.
-  by move->; rewrite ?(abelem_pgroup abelP) // subsetI sPM.
-case: (@tau1_mmaxI_asymmetry M L p P q S q S) => //.
-  by rewrite !inE subsetI sPM sPL abelP dimP.
-by rewrite (pHall_subl _ (subsetIl M L) sylS_M) // subsetI (pHall_sub sylS_M).
-Qed.
-
-(* This is B & G, Theorem 13.10. *)
-Theorem tau13_regular M E E1 E2 E3 p P :
-    M \in 'M -> sigma_complement M E E1 E2 E3 ->
-    P \in 'E_p^1(E1) -> ~~ (P \subset 'C(E3)) ->
-  [/\ (*a*) semiregular E3 E1,
-      (*b*) semiregular M`_\sigma E3
-    & (*c*) 'C_(M`_\sigma)(P) != 1].
-Proof.
-move=> maxM complEi EpP not_cE3P.
-have nsMsM: M`_\sigma <| M := pcore_normal _ M; have [sMsM nMsM] := andP nsMsM.
-have [hallMs sMaMs] := (Msigma_Hall maxM, Malpha_sub_Msigma maxM).
-have [[sE3E' nsE3E] _ [_ cycE3] _ _] := sigma_compl_context maxM complEi.
-have [hallE hallE1 _ hallE3] := complEi.
-have [[_ sM_Ms _] [sEM sM'E _]] := (and3P hallMs, and3P hallE).
-have [[sE1E t1E1 _] [sE3E t3E3 _] _] := (and3P hallE1, and3P hallE3).
-have [sPE1 abelP dimP] := pnElemP EpP; have [pP _ _] := and3P abelP.
-have [ntP t1MP] := (nt_pnElem EpP isT, pgroupS sPE1 t1E1).
-have sPE := subset_trans sPE1 sE1E; have sPM := subset_trans sPE sEM.
-have piPp: p \in \pi(P) by rewrite -p_rank_gt0 p_rank_abelem ?dimP.
-have t1Mp: p \in \tau1(M) := pnatPpi t1MP piPp.
-have [Q sylQ not_cPQ]: exists2 Q, Sylow E3 (gval Q) & ~~ (P \subset 'C(Q)).
-  apply/exists_inP; rewrite -negb_forall_in; apply: contra not_cE3P.
-  move/forall_inP=> cPE3; rewrite centsC -(Sylow_gen E3) gen_subG.
-  by apply/bigcupsP=> Q sylQ; rewrite centsC cPE3.
-have{sylQ} [q q_pr sylQ] := SylowP _ _ sylQ; have [sQE3 qQ _] := and3P sylQ.
-have ntQ: Q :!=: 1 by apply: contraNneq not_cPQ => ->; apply: cents1.
-have t3Mq: q \in \tau3(M).
-  by rewrite (pnatPpi t3E3) // -p_rank_gt0 -(rank_Sylow sylQ) rank_gt0.
-have nQP: P \subset 'N(Q).
-  rewrite (subset_trans sPE) ?normal_norm //.
-  by rewrite (char_normal_trans _ nsE3E) ?sub_cyclic_char.
-have regPQ: 'C_Q(P) = 1.
-  apply: contraNeq not_cPQ; rewrite setIC => /meet_Ohm1.
-  rewrite setIC => /prime_meetG/=/implyP.
-  rewrite (Ohm1_cyclic_pgroup_prime (cyclicS sQE3 cycE3) qQ) // q_pr centsC.
-  apply: (coprime_odd_faithful_Ohm1 qQ) nQP _ (mFT_odd _).
-  exact: sub_pnat_coprime tau3'1 (pgroupS sQE3 t3E3) t1MP.
-have sQE' := subset_trans sQE3 sE3E'.
-have sQM := subset_trans (subset_trans sQE3 sE3E) sEM.
-have [L maxNL] := mmax_exists (mFT_norm_proper ntQ (mFT_pgroup_proper qQ)).
-have [maxL sNQL] := setIdP maxNL; have sQL := subset_trans (normG Q) sNQL.
-have notMGL: gval L \notin M :^: G.
-  by apply: mmax_norm_notJ maxM maxL qQ sQM sNQL _; rewrite t3Mq !orbT.
-have [ntCMaP tiCMaQP]: 'C_(M`_\alpha)(P) != 1 /\ 'C_(M`_\alpha)(Q <*> P) = 1.
-  have EpMP: P \in 'E_p^1(M) by apply/pnElemP.
-  have p'q: q != p by apply: contraNneq (tau3'1 t1Mp) => <-.
-  have [|_ [] //] := cent_Malpha_reg_tau1 maxM t1Mp p'q EpMP ntQ nQP regPQ.
-    by apply: contraTneq maxNL => ->; rewrite inE (contra_orbit _ _ notMGL).
-  have sM'q: q \in \sigma(M)^' by case/andP: t3Mq.
-  exact: subHall_Sylow hallE sM'q (subHall_Sylow hallE3 t3Mq sylQ).
-split=> [x E1x | x E3x |]; last exact: subG1_contra (setSI _ sMaMs) ntCMaP.
-  apply: contraNeq ntCMaP => ntCE3X.
-  have prE31: semiprime M`_\sigma (E3 <*> E1).
-    apply: tau13_primact_Msigma maxM complEi _ => regE13.
-    by rewrite regE13 ?eqxx in ntCE3X.
-  rewrite -subG1 -tiCMaQP /= -(setIidPl sMaMs) -!setIA setIS //.
-  rewrite (cent_semiprime prE31 _ ntP) ?setIS ?centS //=.
-    by rewrite -!genM_join genS ?mulgSS.
-  by rewrite sub_gen // subsetU // sPE1 orbT.
-have prE3 := tau3_primact_Msigma maxM hallE hallE3.
-apply/eqP; apply/idPn; rewrite prE3 {x E3x}// -rank_gt0.
-have [u _ -> ruC] := rank_witness 'C_(M`_\sigma)(E3).
-have sCMs := subsetIl M`_\sigma 'C(E3).
-have sMu: u \in \sigma(M) by rewrite (pnatPpi (pgroupS sCMs _)) -?p_rank_gt0.
-have nCE: E \subset 'N('C_(M`_\sigma)(E3)).
-  by rewrite normsI ?norms_cent ?(normal_norm nsE3E) // (subset_trans sEM).
-have coCE := coprimeSg sCMs (pnat_coprime (pcore_pgroup _ _) sM'E).
-have solC := solvableS (subset_trans sCMs sMsM) (mmax_sol maxM).
-have{nCE coCE solC} [U sylU nUE] := coprime_Hall_exists u nCE coCE solC.
-have ntU: U :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylU).
-have cMsL_Q: Q \subset 'C(M`_\sigma :&: L).
-  have t13q: (q \in \tau1(M)) || (q \in \tau3(M)) by rewrite t3Mq orbT.
-  have [-> //] := cent_norm_tau13_mmax maxM hallE t13q sQM qQ maxNL.
-  by rewrite subsetI sQM.
-rewrite /= -(cent_semiprime prE3 sQE3 ntQ) in sylU.
-have [sUMs cQU] := subsetIP (pHall_sub sylU).
-have{cMsL_Q} sylU_MsL: u.-Sylow(M`_\sigma :&: L) U.
-  apply: pHall_subl sylU; last by rewrite subsetI subsetIl centsC.
-  by rewrite subsetI sUMs (subset_trans (cents_norm _) sNQL).
-have sylU_ML: u.-Sylow(M :&: L) U.
-  apply: subHall_Sylow sMu sylU_MsL.
-  by rewrite /= -(setIidPl sMsM) -setIA (setI_normal_Hall nsMsM) ?subsetIl.
-have [sUML uU _] := and3P sylU_ML; have{sUML} [sUM sUL] := subsetIP sUML.
-have [sNUM regPU]: 'N(U) \subset M /\ 'C_U(P) = 1.
-  have [bMu | bM'u] := boolP (u \in \beta(M)).
-    have [bM_U sMbMa] := (pi_pgroup uU bMu, Mbeta_sub_Malpha M).
-    split; first by rewrite beta_norm_sub_mmax /psubgroup ?sUM.
-    apply/trivgP; rewrite -tiCMaQP centY setIA setSI // subsetI cQU.
-    by rewrite (subset_trans _ sMbMa) // (sub_Hall_pcore (Mbeta_Hall maxM)).
-  have sylU_Ms: u.-Sylow(M`_\sigma) U.
-    have [H hallH cHE'] := der_compl_cent_beta' maxM hallE.
-    rewrite pHallE sUMs (card_Hall sylU) eqn_dvd.
-    rewrite partn_dvd ?cardG_gt0 ?cardSg ?subsetIl //=.
-    rewrite -(@partn_part u \beta(M)^') => [|v /eqnP-> //].
-    rewrite -(card_Hall hallH) partn_dvd ?cardG_gt0 ?cardSg //.
-    by rewrite subsetI (pHall_sub hallH) centsC (subset_trans sQE').
-  split; first exact: norm_sigma_Sylow (subHall_Sylow hallMs sMu sylU_Ms).
-  apply: contraNeq (contra_orbit _ _ notMGL); rewrite -rank_gt0.
-  rewrite (rank_pgroup (pgroupS _ uU)) ?subsetIl // => /p_rank_geP[X] /=.
-  rewrite -(setIidPr sUMs) setIAC pnElemI -setIdE => /setIdP[EuX sXU].
-  have [_ uniqU] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sPE1 ntP EuX.
-  by rewrite (eq_uniq_mmax (uniqU U sylU_Ms) maxL).
-have sPL := subset_trans nQP sNQL.
-have sPML: P \subset M :&: L by apply/subsetIP.
-have t1Lp: p \in \tau1(L).
-  have not_cMsL_P: ~~ (P \subset 'C(M`_\sigma :&: L)).
-    apply: contra ntU => cMsL_P; rewrite -subG1 -regPU subsetIidl.
-    by rewrite centsC (centsS (pHall_sub sylU_MsL)).
-  apply: contraR (not_cMsL_P) => t1L'p.
-  have [piEp piLp] := (piSg sPE piPp, piSg sPL piPp).
-  case: (Msigma_setI_mmax_central maxM hallE maxL piEp piLp) => // [|->] //.
-  apply: contraNneq not_cMsL_P => /commG1P.
-  by rewrite centsC; apply: subset_trans sPML.
-have EpMLP: P \in 'E_p^1(M :&: L) by apply/pnElemP.
-case: (@tau1_mmaxI_asymmetry M L p P q Q u U) => //.
-have [sylQ_E [sM'q _]] := (subHall_Sylow hallE3 t3Mq sylQ, andP t3Mq).
-have sylQ_M := subHall_Sylow hallE sM'q sylQ_E.
-have sQML: Q \subset M :&: L by apply/subsetIP.
-by rewrite (subset_trans sPE nUE) (pHall_subl sQML _ sylQ_M) ?subsetIl.
-Qed.
-
-(* This is B & G, Corollary 13.11. *)
-Corollary tau13_nonregular M E E1 E2 E3 :
-    M \in 'M -> sigma_complement M E E1 E2 E3 -> ~ semiregular M`_\sigma E3 ->
-  [/\ (*a*) E1 :!=: 1,
-      (*b*) E3 ><| E1 = E,
-      (*c*) semiprime M`_\sigma E
-    & (*d*) forall X, X \in 'E^1(E) -> X <| E].
-Proof.
-move=> maxM complEi not_regE3Ms.
-have [hallE hallE1 hallE2 hallE3 _] := complEi.
-have [[sE1E t1E1 _] [sE3E t3E3 _]] := (and3P hallE1, and3P hallE3).
-have{hallE2} E2_1: E2 :==: 1.
-  apply/idPn; rewrite -rank_gt0; have [p _ ->] := rank_witness E2.
-  rewrite p_rank_gt0 => /(pnatPpi (pHall_pgroup hallE2))t2p.
-  have [A Ep2A _] := ex_tau2Elem hallE t2p.
-  by apply: not_regE3Ms; case: (tau2_regular maxM complEi t2p Ep2A).
-have [_ ntE1 [cycE1 cycE3] [defE _] _] := sigma_compl_context maxM complEi.
-rewrite (eqP E2_1) sdprod1g in defE; have{ntE1} ntE1 := ntE1 E2_1.
-have [nsE3E _ mulE31 nE31 _] := sdprod_context defE.
-have cE3E1 P: P \in 'E^1(E1) -> P \subset 'C(E3).
-  by case/nElemP=> p EpP; apply/idPn => /(tau13_regular maxM complEi EpP)[].
-split=> // [|X EpX].
-  rewrite -mulE31 -norm_joinEr //.
-  have [-> | ntE3] := eqsVneq E3 1.
-    by rewrite joing1G; apply: (tau1_primact_Msigma maxM hallE hallE1).
-  apply: tau13_primact_Msigma maxM complEi _ => regE13.
-  have:= ntE1; rewrite -rank_gt0; case/rank_geP=> P EpP.
-  have cPE3: E3 \subset 'C(P) by rewrite centsC cE3E1.
-  have [p Ep1P] := nElemP EpP; have [sPE1 _ _] := pnElemP Ep1P.
-  have ntP: P :!=: 1 by apply: (nt_pnElem Ep1P).
-  by case/negP: ntE3; rewrite -(setIidPl cPE3) (cent_semiregular regE13 _ ntP).
-have [p Ep1X] := nElemP EpX; have [sXE abelX oX] := pnElemPcard Ep1X.
-have [p_pr ntX] := (pnElem_prime Ep1X, nt_pnElem Ep1X isT).
-have tau31p: p \in [predU \tau3(M) & \tau1(M)].
-  rewrite (pgroupP (pgroupS sXE _)) ?oX // -mulE31 pgroupM.
-  rewrite (sub_pgroup _ t3E3) => [|q t3q]; last by rewrite inE /= t3q.
-  by rewrite (sub_pgroup _ t1E1) // => q t1q; rewrite inE /= t1q orbT.
-have [/= t3p | t1p] := orP tau31p.
-  rewrite (char_normal_trans _ nsE3E) ?sub_cyclic_char //.
-  by rewrite (sub_normal_Hall hallE3) // (pi_pgroup (abelem_pgroup abelX)).
-have t1X := pi_pgroup (abelem_pgroup abelX) t1p.
-have [e Ee sXeE1] := Hall_Jsub (sigma_compl_sol hallE) hallE1 sXE t1X.
-rewrite /normal sXE -(conjSg _ _ e) conjGid //= -normJ -mulE31 mulG_subG.
-rewrite andbC sub_abelian_norm ?cyclic_abelian ?cents_norm // centsC cE3E1 //.
-rewrite -(setIidPr sE1E) nElemI !inE sXeE1 andbT.
-by rewrite -(pnElemJ e) conjGid // def_pnElem in Ep1X; case/setIP: Ep1X.
-Qed.
-
-(* This is B & G, Lemma 13.12. *)
-Lemma tau12_regular M E p q P A :
-    M \in 'M -> \sigma(M)^'.-Hall(M) E ->
-    p \in \tau1(M) -> P \in 'E_p^1(E) -> q \in \tau2(M) -> A \in 'E_q^2(E) ->
-    'C_A(P) != 1 ->
-  'C_(M`_\sigma)(P) = 1.
-Proof.
-move=> maxM hallE t1p EpP t2q Eq2A ntCAP; apply: contraNeq (ntCAP) => ntCMsP.
-have [[nsAE _] _ uniq_cMs _] := tau2_compl_context maxM hallE t2q Eq2A.
-have [sPE abelP dimP] := pnElemP EpP; have [pP _] := andP abelP.
-have ntP: P :!=: 1 by apply: nt_pnElem EpP _.
-have [solE t1P] := (sigma_compl_sol hallE, pi_pgroup pP t1p).
-have [E1 hallE1 sPE1] := Hall_superset solE sPE t1P.
-have [_ [E3 hallE3]] := ex_tau13_compl hallE.
-have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3.
-have not_cAP: ~~ (P \subset 'C(A)).
-  have [_ regCE1A _] := tau2_regular maxM complEi t2q Eq2A.
-  apply: contra ntCMsP => cAP; rewrite (cent_semiregular regCE1A _ ntP) //.
-  exact/subsetIP.
-have [sAE abelA dimA] := pnElemP Eq2A; have [qA _] := andP abelA.
-pose Y := 'C_A(P)%G; have{abelA dimA} EqY: Y \in 'E_q^1('C_E(P)).
-  have sYA: Y \subset A := subsetIl A _; have abelY := abelemS sYA abelA.
-  rewrite !inE setSI // abelY eqn_leq -{2}rank_abelem // rank_gt0 -ltnS -dimA.
-  by rewrite properG_ltn_log //= /proper subsetIl subsetIidl centsC.
-have ntCMsY: 'C_(M`_\sigma)(Y) != 1.
-  by apply: subG1_contra ntCMsP; apply: cent_tau1Elem_Msigma t1p EpP EqY.
-have EqEY: Y \in 'E_q^1(E) by rewrite pnElemI in EqY; case/setIP: EqY.
-have uniqCY := uniq_cMs _ EqEY ntCMsY.
-have [ntA nAE] := (nt_pnElem Eq2A isT, normal_norm nsAE).
-have [L maxNL] := mmax_exists (mFT_norm_proper ntA (mFT_pgroup_proper qA)).
-have [sLq t12Lp]: q \in \sigma(L) /\ (p \in \tau1(L)) || (p \in \tau2(L)).
-  have [sLt2 t12cA' _] := primes_norm_tau2Elem maxM hallE t2q Eq2A maxNL.
-  split; first by have /andP[] := sLt2 q t2q.
-  apply: pnatPpi (pgroupS (quotientS _ sPE) t12cA') _.
-  rewrite -p_rank_gt0 -rank_pgroup ?quotient_pgroup // rank_gt0.
-  rewrite -subG1 quotient_sub1 ?subsetI ?sPE // (subset_trans sPE) //.
-  by rewrite normsI ?normG ?norms_cent.
-have [maxL sNL] := setIdP maxNL; have sEL := subset_trans nAE sNL.
-have sL'p: p \in \sigma(L)^' by move: t12Lp; rewrite -andb_orr => /andP[].
-have [sPL sL'P] := (subset_trans sPE sEL, pi_pgroup pP sL'p).
-have{sL'P} [F hallF sPF] := Hall_superset (mmax_sol maxL) sPL sL'P.
-have solF := sigma_compl_sol hallF.
-have [sAL sL_A] := (subset_trans (normG A) sNL, pi_pgroup qA sLq).
-have sALs: A \subset L`_\sigma by rewrite (sub_Hall_pcore (Msigma_Hall maxL)).
-have neqLM: L != M by apply: contraTneq sLq => ->; case/andP: t2q.
-have{t12Lp} [t1Lp | t2Lp] := orP t12Lp.
-  have [F1 hallF1 sPF1] := Hall_superset solF sPF (pi_pgroup pP t1Lp).
-  have EqLsY: Y \in 'E_q^1('C_(L`_\sigma)(P)).
-    by rewrite !inE setSI //; case/pnElemP: EqY => _ -> ->.
-  have [defL _] := cent_cent_Msigma_tau1_uniq maxL hallF hallF1 sPF1 ntP EqLsY.
-  by rewrite -in_set1 -uniqCY defL set11 in neqLM.
-have sCPL: 'C(P) \subset L.
-  have [B Ep2B _] := ex_tau2Elem hallF t2Lp.
-  have EpFP: P \in 'E_p^1(F) by apply/pnElemP.
-  have [_ _ uniq_cLs _] := tau2_compl_context maxL hallF t2Lp Ep2B.
-  by case/mem_uniq_mmax: (uniq_cLs _ EpFP (subG1_contra (setSI _ sALs) ntCAP)).
-have Eq2MA: A \in 'E_q^2(M).
-  by move: Eq2A; rewrite -(setIidPr (pHall_sub hallE)) pnElemI => /setIP[].
-have [_ _ _ tiMsL _] := tau2_context maxM t2q Eq2MA.
-by case/negP: ntCMsP; rewrite -subG1 -(tiMsL L) ?setIS // 3!inE neqLM maxL.
-Qed.
-
-(* This is B & G, Lemma 13.13. *)
-Lemma tau13_nonregular_sigma M E p P :
-    M \in 'M -> \sigma(M)^'.-Hall(M) E ->
-    P \in 'E_p^1(E) -> (p \in \tau1(M)) || (p \in \tau3(M)) ->
-    'C_(M`_\sigma)(P) != 1 ->
-  {in 'M('N(P)), forall Mstar, p \in \sigma(Mstar)}.
-Proof.
-move=> maxM hallE EpP t13Mp ntCMsP L maxNL /=.
-have [maxL sNL] := setIdP maxNL.
-have [sPE abelP dimP] := pnElemP EpP; have [pP _] := andP abelP.
-have [solE ntP] := (sigma_compl_sol hallE, nt_pnElem EpP isT).
-have /orP[// | t2Lp] := prime_class_mmax_norm maxL pP sNL.
-have:= ntCMsP; rewrite -rank_gt0 => /rank_geP[Q /nElemP[q EqQ]].
-have [sQcMsP abelQ dimQ] := pnElemP EqQ; have [sQMs cPQ] := subsetIP sQcMsP.
-have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 p_rank_abelem ?dimQ.
-have sMq: q \in \sigma(M) := pnatPpi (pgroupS sQMs (pcore_pgroup _ M)) piQq.
-have rpM: 'r_p(M) = 1%N by move: t13Mp; rewrite -2!andb_orr andbCA; case: eqP.
-have sL'q: q \notin \sigma(L).
-  have notMGL: gval L \notin M :^: G.
-    by apply: contraL t2Lp => /imsetP[x _ ->]; rewrite tau2J 2!inE rpM andbF.
-  by apply: contraFN (sigma_partition maxM maxL notMGL q) => sLq; apply/andP.
-have [[sL'p _] [qQ _]] := (andP t2Lp, andP abelQ).
-have sL'PQ: \sigma(L)^'.-group (P <*> Q).
-  by rewrite cent_joinEr // pgroupM (pi_pgroup pP) // (pi_pgroup qQ).
-have sPQ_L: P <*> Q \subset L.
-  by rewrite (subset_trans _ sNL) // join_subG normG cents_norm.
-have{sPQ_L sL'PQ} [F hallF sPQF] := Hall_superset (mmax_sol maxL) sPQ_L sL'PQ.
-have{sPQF} [sPF sQF] := joing_subP sPQF.
-have [A Ep2A _] := ex_tau2Elem hallF t2Lp.
-have [[nsAF defA1] _ _ _] := tau2_compl_context maxL hallF t2Lp Ep2A.
-have EpAP: P \in 'E_p^1(A) by rewrite -defA1; apply/pnElemP.
-have{EpAP} sPA: P \subset A by case/pnElemP: EpAP.
-have sCQM: 'C(Q) \subset M.
-  suffices: 'M('C(Q)) = [set M] by case/mem_uniq_mmax.
-  have [t1Mp | t3Mp] := orP t13Mp.
-    have [E1 hallE1 sPE1] := Hall_superset solE sPE (pi_pgroup pP t1Mp).
-    by have [] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sPE1 ntP EqQ.
-  have [E3 hallE3 sPE3] := Hall_superset solE sPE (pi_pgroup pP t3Mp).
-  have [[E1 hallE1] _] := ex_tau13_compl hallE; have [sE1E _] := andP hallE1.
-  have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3.
-  have [regE3 | ntE1 _ prE _] := tau13_nonregular maxM complEi.
-    by rewrite (cent_semiregular regE3 sPE3 ntP) eqxx in ntCMsP.
-  rewrite /= (cent_semiprime prE) // -(cent_semiprime prE sE1E ntE1) in EqQ.
-  by have [] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 _ ntE1 EqQ.
-have not_cQA: ~~ (A \subset 'C(Q)).
-  have [_ abelA dimA] := pnElemP Ep2A; apply: contraFN (ltnn 1) => cQA.
-  by rewrite -dimA -p_rank_abelem // -rpM p_rankS ?(subset_trans cQA sCQM).
-have t1Lq: q \in \tau1(L).
-  have [_ nsCF t1Fb] :=  tau1_cent_tau2Elem_factor maxL hallF t2Lp Ep2A.
-  rewrite (pnatPpi (pgroupS (quotientS _ sQF) t1Fb)) //.
-  rewrite -p_rank_gt0 -rank_pgroup ?quotient_pgroup // rank_gt0.
-  rewrite -subG1 quotient_sub1 ?(subset_trans _ (normal_norm nsCF)) //.
-  by rewrite subsetI sQF centsC.
-have defP: 'C_A(Q) = P.
-  apply/eqP; rewrite eq_sym eqEcard subsetI sPA centsC cPQ /=.
-  have [_ abelA dimA] := pnElemP Ep2A; have [pA _] := andP abelA.
-  rewrite (card_pgroup (pgroupS _ pA)) ?subsetIl // (card_pgroup pP) dimP.
-  rewrite leq_exp2l ?prime_gt1 ?(pnElem_prime EpP) //.
-  by rewrite -ltnS -dimA properG_ltn_log // /proper subsetIl subsetIidl.
-have EqFQ: Q \in 'E_q^1(F) by apply/pnElemP.
-have regQLs: 'C_(L`_\sigma)(Q) = 1.
-  by rewrite (tau12_regular maxL hallF t1Lq EqFQ t2Lp Ep2A) // defP.
-have ntAQ: [~: A, Q] != 1 by rewrite (sameP eqP commG1P).
-have [_ _ [_]] := tau1_act_tau2 maxL hallF t2Lp Ep2A t1Lq EqFQ regQLs ntAQ.
-by case/negP; rewrite /= defP (subset_trans (cent_sub P)).
-Qed.
-
-End Section13.
-