Timings for BGsection11.v

(* (c) Copyright 2006-2015 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.
From mathcomp
Require Import BGsection1 BGsection3 BGsection4 BGsection5 BGsection6.
From mathcomp
Require Import BGsection7 BGsection10.

(******************************************************************************)
(*   This file covers B & G, section 11; it has only one definition:          *)
(*    exceptional_FTmaximal p M A0 A <=>                                      *)
(*      p, M and A0 satisfy the conditions of Hypothesis 11.1 in B & G, i.e., *)
(*      M is an "exceptional" maximal subgroup in the terminology of B & G.   *)
(*      In addition, A is elementary abelian p-subgroup of M of rank 2, that  *)
(*      contains A0. The existence of A is guaranteed by Lemma 10.5, but as   *)
(*      in the only two lemmas that make use of the results in this section   *)
(*      (Lemma 12.3 and Theorem 12.5) A is known, we elected to make the      *)
(*      dependency on A explicit.                                             *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope.

Section Section11.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).

Implicit Types p q r : nat.
Implicit Types A E H K M N P Q R S T U V W X Y : {group gT}.

Variables (p : nat) (M A0 A P : {group gT}).

(* This definition corresponsd to Hypothesis 11.1, where the condition on A   *)
(* has been made explicit.                                                    *)
Definition exceptional_FTmaximal :=
  [/\ p \in \sigma(M)^', A \in 'E_p^2(M), A0 \in 'E_p^1(A) & 'N(A0) \subset M].

Hypotheses (maxM : M \in 'M) (excM : exceptional_FTmaximal).
Hypotheses (sylP : p.-Sylow(M) P) (sAP : A \subset P).

(* Splitting the excM hypothesis. *)
Let sM'p : p \in \sigma(M)^'. Proof. by case: excM. Qed.
Let Ep2A : A \in 'E_p^2(M). Proof. by case: excM. Qed.
Let Ep1A0 : A0 \in 'E_p^1(A). Proof. by case: excM. Qed.
Let sNA0_M : 'N(A0) \subset M. Proof. by case: excM. Qed.

(* Arithmetics of p. *)
Let p_pr : prime p := pnElem_prime Ep2A.
Let p_gt1 : p > 1 := prime_gt1 p_pr.
Let p_gt0 : p > 0 := prime_gt0 p_pr.

(* Group orders. *)
Let oA : #|A| = (p ^ 2)%N := card_pnElem Ep2A.
Let oA0 : #|A0| = p := card_pnElem Ep1A0.

(* Structure of A. *)
Let abelA : p.-abelem A. Proof. by case/pnElemP: Ep2A. Qed.
Let pA : p.-group A := abelem_pgroup abelA.
Let cAA : abelian A := abelem_abelian abelA.

(* Various set inclusions. *)
Let sA0A : A0 \subset A. Proof. by case/pnElemP: Ep1A0. Qed.
Let sPM : P \subset M := pHall_sub sylP.
Let sAM : A \subset M := subset_trans sAP sPM.
Let sCA0_M : 'C(A0) \subset M := subset_trans (cent_sub A0) sNA0_M.
Let sCA_M : 'C(A) \subset M := subset_trans (centS sA0A) sCA0_M.

(* Alternative E_p^1 memberships for A0; the first is the one used to state   *)
(* Hypothesis 11.1 in B & G, the second is the form expected by Lemma 10.5.   *)
(* Note that #|A0| = p (oA0 above) would wokr just as well.                   *)
Let Ep1A0_M : A0 \in 'E_p^1(M) := subsetP (pnElemS p 1 sAM) A0 Ep1A0.
Let Ep1A0_G : A0 \in 'E_p^1(G) := subsetP (pnElemS p 1 (subsetT M)) A0 Ep1A0_M.

(* This does not depend on exceptionalM, and could move to Section 10. *)
Lemma sigma'_Sylow_contra : p \in \sigma(M)^' -> ~~ ('N(P) \subset M).
Proof. by apply: contra => sNM; apply/exists_inP; exists P. Qed.

(* First preliminary remark of Section 11; only depends on sM'p and sylP. *)
Let not_sNP_M: ~~ ('N(P) \subset M) := sigma'_Sylow_contra sM'p.

(* Second preliminary remark of Section 11; only depends on sM'p, Ep1A0_M,    *)
(* and sNA0_M.                                                                *)
Lemma p_rank_exceptional : 'r_p(M) = 2.
Proof. exact: sigma'_norm_mmax_rank2 (pgroupS sA0A pA) _. Qed.
Let rM := p_rank_exceptional.

(* Third preliminary remark of Section 11. *)
Lemma exceptional_pmaxElem : A \in 'E*_p(G).
Proof.
have [_ _ dimA]:= pnElemP Ep2A.
apply/pmaxElemP; split=> [|E EpE sAE]; first by rewrite !inE subsetT.
have [//|ltAE]: A :=: E \/ A \proper E := eqVproper sAE.
have [_ abelE] := pElemP EpE; have [pE cEE _] := and3P abelE.
suffices: logn p #|E| <= 'r_p(M) by rewrite leqNgt rM -dimA properG_ltn_log.
by rewrite logn_le_p_rank // inE (subset_trans cEE) ?(subset_trans (centS sAE)).
Qed.
Let EpmA := exceptional_pmaxElem.

(* This is B & G, Lemma 11.1. *)
Lemma exceptional_TIsigmaJ g q Q1 Q2 :
    g \notin M -> A \subset M :^ g ->
    q.-Sylow(M`_\sigma) Q1 ->  A \subset 'N(Q1) ->
    q.-Sylow(M`_\sigma :^ g) Q2 -> A \subset 'N(Q2) ->
     (*a*) Q1 :&: Q2 = 1
  /\ (*b*) (forall X, X \in 'E_p^1(A) -> 'C_Q1(X) = 1 \/ 'C_Q2(X) = 1).
Proof.
move=> notMg sAMg sylQ1 nQ1A sylQ2 nQ2A.
have [-> | ntQ1] := eqsVneq Q1 1.
  by split=> [|? _]; last left; apply: (setIidPl (sub1G _)).
have [sQ1Ms qQ1 _] := and3P sylQ1.
have{qQ1} [q_pr q_dv_Q1 _] := pgroup_pdiv qQ1 ntQ1.
have{sQ1Ms q_dv_Q1} sMq: q \in \sigma(M).
  exact: pgroupP (pgroupS sQ1Ms (pcore_pgroup _ _)) q q_pr q_dv_Q1.
have{sylQ1} sylQ1: q.-Sylow(M) Q1.
  by rewrite (subHall_Sylow (Msigma_Hall maxM)).
have sQ1M := pHall_sub sylQ1.
have{sylQ2} sylQ2g': q.-Sylow(M) (Q2 :^ g^-1).
  by rewrite (subHall_Sylow (Msigma_Hall _)) // -(pHallJ2 _ _ _ g) actKV.
have sylQ2: q.-Sylow(G) Q2.
  by rewrite -(pHallJ _ _ (in_setT g^-1)) (sigma_Sylow_G maxM).
suffices not_Q1_CA_Q2: gval Q2 \notin Q1 :^: 'O_\pi(A)^'('C(A)).
  have ncA: normed_constrained A.
    have ntA: A :!=: 1 by rewrite -cardG_gt1 oA (ltn_exp2l 0).
    exact: plength_1_normed_constrained ntA EpmA (mFT_proper_plength1 _).
  have q'A: q \notin \pi(A).
    by apply: contraL sMq; move/(pnatPpi pA); move/eqnP->.
  have maxnAq Q: q.-Sylow(G) Q -> A \subset 'N(Q) -> Q \in |/|*(A; q).
    move=> sylQ; case/(max_normed_exists (pHall_pgroup sylQ)) => R maxR sQR.
    have [qR _] := mem_max_normed maxR.
    by rewrite -(group_inj (sub_pHall sylQ qR sQR (subsetT R))).
  have maxQ1 := maxnAq Q1 (sigma_Sylow_G maxM sMq sylQ1) nQ1A.
  have maxQ2 := maxnAq Q2 sylQ2 nQ2A.
  have transCAQ := normed_constrained_meet_trans ncA q'A _ _ maxQ1 maxQ2.
  split=> [|X EpX].
    apply: contraNeq not_Q1_CA_Q2 => ntQ12; apply/imsetP.
    apply: transCAQ (sAM) (mmax_proper maxM) _ _.
      by rewrite (setIidPl sQ1M).
    by apply: contraNneq ntQ12 => tiQ2M; rewrite setIC -subG1 -tiQ2M setIS.
  apply/pred2P; apply: contraR not_Q1_CA_Q2; case/norP=> ntCQ1 ntCQ2.
  have [sXA _ oX] := pnElemPcard EpX.
  apply/imsetP; apply: transCAQ (centSS _ sXA cAA) _ ntCQ1 ntCQ2 => //.
  by rewrite mFT_cent_proper // -cardG_gt1 oX prime_gt1.
apply: contra notMg; case/imsetP=> k cAk defQ2.
have{cAk} Mk := subsetP sCA_M k (subsetP (pcore_sub _ _) k cAk).
have{k Mk defQ2} sQ2M: Q2 \subset M by rewrite defQ2 conj_subG.
have [sQ2g'M qQ2g' _] := and3P sylQ2g'.
by rewrite (sigma_Sylow_trans _ sylQ2g') // actKV.
Qed.

(* This is B & G, Corollary 11.2. *)
Corollary exceptional_TI_MsigmaJ g :
  g \notin M -> A \subset M :^ g ->
    (*a*) M`_\sigma :&: M :^ g = 1
 /\ (*b*) M`_\sigma :&: 'C(A0 :^ g) = 1.
Proof.
move=> notMg sAMg; set Ms := M`_\sigma; set H := [group of Ms :&: M :^ g].
have [H1 | ntH] := eqsVneq H 1.
  by split=> //; apply/trivgP; rewrite -H1 setIS //= centJ conjSg.
pose q := pdiv #|H|.
suffices: #|H|`_q == 1%N by rewrite p_part_eq1 pi_pdiv cardG_gt1 ntH.
have nsMsM: Ms <| M := pcore_normal _ _; have [_ nMsM] := andP nsMsM.
have sHMs: H \subset Ms := subsetIl _ _.
have sHMsg: H \subset Ms :^ g.
  rewrite -sub_conjgV (sub_Hall_pcore (Msigma_Hall _)) //.
    by rewrite pgroupJ (pgroupS sHMs) ?pcore_pgroup.
  by rewrite sub_conjgV subsetIr.
have nMsA := subset_trans sAM nMsM.
have nHA: A \subset 'N(H) by rewrite normsI // normsG.
have nMsgA: A \subset 'N(Ms :^ g) by rewrite normJ (subset_trans sAMg) ?conjSg.
have coMsA: coprime #|Ms| #|A|.
  by rewrite oA coprime_expr ?(pnat_coprime (pcore_pgroup _ _)) ?pnatE.
have coHA: coprime #|H| #|A| := coprimeSg sHMs coMsA.
have coMsgA: coprime #|Ms :^ g| #|A| by rewrite cardJg.
have solA: solvable A := abelian_sol cAA.
have [Q0 sylQ0 nQ0A] := sol_coprime_Sylow_exists q solA nHA coHA.
have [sQ0H qQ0 _] := and3P sylQ0.
have supQ0 := sol_coprime_Sylow_subset _ _ solA (subset_trans sQ0H _) qQ0 nQ0A.
have [Q1 [sylQ1 nQ1A sQ01]] := supQ0 _ nMsA coMsA sHMs.
have [Q2 [sylQ2 nQ2A sQ02]] := supQ0 _ nMsgA coMsgA sHMsg.
have tiQ12: Q1 :&: Q2 = 1.
  by have [-> _] := exceptional_TIsigmaJ notMg sAMg sylQ1 nQ1A sylQ2 nQ2A.
by rewrite -(card_Hall sylQ0) -trivg_card1 -subG1 -tiQ12 subsetI sQ01.
Qed.

(* This is B & G, Theorem 11.3. *)
Theorem exceptional_sigma_nil : nilpotent M`_\sigma.
Proof.
have [g nPg notMg] := subsetPn not_sNP_M.
set Ms := M`_\sigma; set F := Ms <*> A0 :^ g.
have sA0gM: A0 :^ g \subset M.
  by rewrite (subset_trans _ sPM) // -(normP nPg) conjSg (subset_trans sA0A).
have defF: Ms ><| A0 :^ g = F.
  rewrite sdprodEY ?coprime_TIg //.
    by rewrite (subset_trans sA0gM) ?gFnorm.
  by rewrite cardJg oA0 (pnat_coprime (pcore_pgroup _ _)) ?pnatE.
have regA0g: 'C_Ms(A0 :^ g) = 1.
  case/exceptional_TI_MsigmaJ: notMg => //.
  by rewrite -sub_conjgV (subset_trans _ sPM) // sub_conjgV (normP _).
rewrite (prime_Frobenius_sol_kernel_nil defF) ?cardJg ?oA0 //.
by rewrite (solvableS _ (mmax_sol maxM)) // join_subG pcore_sub.
Qed.

(* This is B & G, Corollary 11.4. *)
Corollary exceptional_sigma_uniq H :
  H \in 'M(A) -> H`_\sigma :&: M `_\sigma != 1 -> H :=: M.
Proof.
rewrite setIC => /setIdP[maxH sAH] ntMsHs.
have [g _ defH]: exists2 g, g \in G & H :=: M :^ g.
  apply/imsetP; apply: contraR ntMsHs => /sigma_disjoint[] // _ _.
  by case/(_ exceptional_sigma_nil)=> ->.
rewrite defH conjGid //; apply: contraR ntMsHs => notMg.
have [|tiMsMg _] := exceptional_TI_MsigmaJ notMg; first by rewrite -defH.
by rewrite -subG1 -tiMsMg -defH setIS ?pcore_sub.
Qed.

(* This is B & G, Theorem 11.5. *)
Theorem exceptional_Sylow_abelian P1 : p.-Sylow(M) P1 -> abelian P1.
Proof.
have nregA Q: gval Q != 1 -> A \subset 'N(Q) -> coprime #|Q| #|A| ->
  exists2 X, X \in 'E_p^1(A) & 'C_Q(X) != 1.
- move=> ntQ nQA coQA; apply/exists_inP; apply: contraR ntQ.
  rewrite negb_exists_in -subG1; move/forall_inP=> regA.
  have ncycA: ~~ cyclic A by rewrite (abelem_cyclic abelA) oA pfactorK.
  rewrite -(coprime_abelian_gen_cent1 _ _ nQA) // gen_subG.
  apply/bigcupsP=> x /setD1P[ntx Ax].
  apply/negPn; rewrite /= -cent_cycle subG1 regA // p1ElemE // !inE.
  by rewrite cycle_subG Ax /= -orderE (abelem_order_p abelA).
suffices{P1} cPP: abelian P.
  by move=> sylP1; have [m _ ->] := Sylow_trans sylP sylP1; rewrite abelianJ.
have [g nPg notMg] := subsetPn not_sNP_M.
pose Ms := M`_\sigma; pose q := pdiv #|Ms|; have pP := pHall_pgroup sylP.
have nMsP: P \subset 'N(Ms) by rewrite (subset_trans sPM) ?gFnorm.
have coMsP: coprime #|Ms| #|P|.
  exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat pP sM'p).
have [Q1 sylQ1 nQ1P]:= sol_coprime_Sylow_exists q (pgroup_sol pP) nMsP coMsP.
have ntQ1: Q1 :!=: 1.
  rewrite -cardG_gt1 (card_Hall sylQ1) p_part_gt1 pi_pdiv cardG_gt1.
  by rewrite Msigma_neq1.
have nQ1A: A \subset 'N(Q1) := subset_trans sAP nQ1P.
have coQ1A: coprime #|Q1| #|A|.
  by rewrite (coprimeSg (pHall_sub sylQ1)) // (coprimegS sAP).
have [X1 EpX1 nregX11] := nregA _ ntQ1 nQ1A coQ1A.
pose Q2 := Q1 :^ g; have sylQ2: q.-Sylow(Ms :^ g) Q2 by rewrite pHallJ2.
have{ntQ1} ntQ2: Q2 != 1 by rewrite -!cardG_gt1 cardJg in ntQ1 *.
have nQ2A: A \subset 'N(Q2) by rewrite (subset_trans sAP) ?norm_conj_norm.
have{coQ1A} coQ2A: coprime #|Q2| #|A| by rewrite cardJg. 
have{nregA ntQ2 coQ2A} [X2 EpX2 nregX22] := nregA _ ntQ2 nQ2A coQ2A.
have [|_ regA]:= exceptional_TIsigmaJ notMg _ sylQ1 nQ1A sylQ2 nQ2A.
  by rewrite (subset_trans sAP) // -(normP nPg) conjSg.
have regX21: 'C_Q1(X2) = 1 by case: (regA X2) nregX22 => // ->; rewrite eqxx.
have regX12: 'C_Q2(X1) = 1 by case: (regA X1) nregX11 => // ->; rewrite eqxx.
pose X := 'Ohm_1('Z(P))%G.
have eqCQ12_X: ('C_Q1(X) == 1) = ('C_Q2(X) == 1).
  rewrite -(inj_eq (@conjsg_inj _ g)) conjs1g conjIg -/Q2 -centJ (normP _) //.
  by rewrite (subsetP (gFnorm_trans _ _) g nPg) ?gFnorms.
have{EpX1} EpX1: X1 \in 'E_p^1(A) :\ X.
  rewrite 2!inE EpX1 andbT; apply: contraNneq nregX11 => defX1.
  by rewrite defX1 eqCQ12_X -defX1 regX12.
have{EpX2 eqCQ12_X} EpX2: X2 \in 'E_p^1(A) :\ X.
  rewrite 2!inE EpX2 andbT; apply: contraNneq nregX22 => defX2.
  by rewrite defX2 -eqCQ12_X -defX2 regX21.
apply: contraR nregX11 => not_cPP.
have{not_cPP} transNPA: [transitive 'N_P(A), on 'E_p^1(A) :\ X | 'JG].
  have [|_ _]:= basic_p2maxElem_structure _ pP sAP not_cPP; last by [].
  by rewrite inE (subsetP (pnElemS p 2 (subsetT M))).
have [y PnAy ->] := atransP2 transNPA EpX2 EpX1; have [Py _] := setIP PnAy.
by rewrite centJ -(normsP nQ1P y Py) -conjIg regX21 conjs1g.
Qed.

(* This is B & G, Corollary 11.6. *)
Corollary exceptional_structure (Ms := M`_\sigma) :
  [/\ (*a*) A :=: 'Ohm_1(P),
      (*b*) 'C_Ms(A) = 1
    & (*c*) exists2 A1, A1 \in 'E_p^1(A) & exists2 A2, A2 \in 'E_p^1(A) &
            [/\ A1 :!=: A2, 'C_Ms(A1) = 1 & 'C_Ms(A2) = 1]].
Proof.
pose iMNA := #|'N(A) : M|.
have defA: A :=: 'Ohm_1(P).
  apply/eqP; rewrite eqEcard -{1}(Ohm1_id abelA) OhmS //= oA -rM.
  rewrite -(p_rank_Sylow sylP) p_rank_abelian ?exceptional_Sylow_abelian //.
  by rewrite -card_pgroup // (pgroupS _ (pHall_pgroup sylP)) ?Ohm_sub.
have iMNAgt1: iMNA > 1.
  rewrite indexg_gt1 defA; apply: contra (subset_trans _) not_sNP_M.
  by rewrite char_norms ?Ohm_char.
have iMNAgt2: iMNA > 2.
  pose q := pdiv iMNA; have q_iMNA: q %| iMNA := pdiv_dvd iMNA.
  rewrite (leq_trans _ (dvdn_leq (ltnW _) q_iMNA)) // ltn_neqAle eq_sym.
  rewrite (sameP eqP (prime_oddPn _)) ?prime_gt1 ?pdiv_prime //.
  by rewrite (dvdn_odd q_iMNA) // (dvdn_odd (dvdn_indexg _ _)) ?mFT_odd.
rewrite [iMNA](cardD1 (gval M)) orbit_refl !ltnS lt0n in iMNAgt1 iMNAgt2.
have{iMNAgt1} [Mg1 /= NM_Mg1] := pred0Pn iMNAgt1.
rewrite (cardD1 Mg1) inE /= NM_Mg1 ltnS lt0n in iMNAgt2.
have{iMNAgt2} [Mg2 /= NM_Mg2] := pred0Pn iMNAgt2.
case/andP: NM_Mg1 => neM_Mg1 /rcosetsP[g1 nAg1 defMg1].
have{neM_Mg1} notMg1: g1 \notin M.
  by apply: contra neM_Mg1 => M_g1; rewrite defMg1 rcoset_id.
case/and3P: NM_Mg2 => neMg12 neM_Mg2 /rcosetsP[g2 nAg2 defMg2].
have{neM_Mg2} notMg2: g2 \notin M.
  by apply: contra neM_Mg2 => M_g2; rewrite defMg2 rcoset_id.
pose A1 := (A0 :^ g1)%G; pose A2 := (A0 :^ g2)%G.
have EpA1: A1 \in 'E_p^1(A) by rewrite -(normP nAg1) pnElemJ.
have EpA2: A2 \in 'E_p^1(A) by rewrite -(normP nAg2) pnElemJ.
have{neMg12} neqA12: A1 :!=: A2.
  rewrite -(canF_eq (conjsgKV g2)) -conjsgM (sameP eqP normP).
  rewrite (contra (subsetP sNA0_M _)) // -mem_rcoset.
  by apply: contra neMg12 => g1Mg2; rewrite defMg1 defMg2 (rcoset_eqP g1Mg2).
have{notMg1 nAg1} regA1: 'C_Ms(A1) = 1.
  by case/exceptional_TI_MsigmaJ: notMg1; rewrite // -(normP nAg1) conjSg.
have{notMg2 nAg2} regA2: 'C_Ms(A2) = 1.
  by case/exceptional_TI_MsigmaJ: notMg2; rewrite // -(normP nAg2) conjSg.
split=> //; last by exists A1 => //; exists A2 => //.
by apply/trivgP; rewrite -regA1 setIS ?centS //; case/pnElemP: EpA1.
Qed.

(* This is B & G, Theorem 11.7 (the main result on exceptional subgroups). *)
Theorem exceptional_mul_sigma_normal : M`_\sigma <*> A <| M.
Proof.
set Ms := M`_\sigma; have pP := pHall_pgroup sylP; have solM := mmax_sol maxM.
have [E hallE sPE] := Hall_superset solM sPM (pi_pnat pP sM'p).
have sAE := subset_trans sAP sPE; have [sEM s'E _] := and3P hallE.
have [_ _ dimA] := pnElemP Ep2A.
have rE: 'r(E) = 2.
  apply/eqP; rewrite eqn_leq -{2}dimA -rank_abelem ?rankS // andbT leqNgt.
  have [q q_pr ->]:= rank_witness E; apply/negP=> rqEgt2.
  have piEq: q \in \pi(E) by rewrite -p_rank_gt0 -(subnKC rqEgt2).
  case/negP: (pnatPpi s'E piEq); rewrite /= alpha_sub_sigma // !inE.
  by rewrite (leq_trans rqEgt2) ?p_rankS.
have rFEle2: 'r('F(E)) <= 2 by rewrite -rE rankS ?Fitting_sub.
have solE := solvableS sEM solM; have oddE := mFT_odd E.
pose tau : nat_pred := [pred q | q > p]; pose K := 'O_tau(E).
have hallK: tau.-Hall(E) K by rewrite rank2_ge_pcore_Hall.
pose ptau : nat_pred := [pred q | q >= p]; pose KP := K <*> P.
have nKP: P \subset 'N(K) by rewrite (subset_trans sPE) ?gFnorm.
have coKP: coprime #|K| #|P|.
  by rewrite (pnat_coprime (pcore_pgroup _ _)) ?(pi_pnat pP) //= !inE ltnn.
have hallKP: ptau.-Hall(E) KP.
  rewrite pHallE join_subG pcore_sub sPE /= norm_joinEr ?coprime_cardMg //.
  apply/eqP; rewrite -(partnC tau (part_gt0 _ _)) (card_Hall sylP).
  rewrite (card_Hall hallK) partn_part => [|q]; last exact: leqW.
  rewrite (card_Hall hallE) -!partnI; congr (_ * _)%N; apply: eq_partn => q.
  by rewrite 4!inE andbC /= 8!inE -leqNgt -eqn_leq eq_sym; case: eqP => // <-.
have nsKP_E: KP <| E.
  by rewrite [KP](eq_Hall_pcore _ hallKP) ?pcore_normal ?rank2_ge_pcore_Hall.
have [cKA | not_cKA]:= boolP (A \subset 'C(K)).
  pose KA := K <*> A; have defKA: K \x A = KA.
    by rewrite dprodEY // coprime_TIg // (coprimegS sAP).
  have defA: 'Ohm_1(P) = A by case exceptional_structure.
  have{defA} defA: 'Ohm_1('O_p(KP)) = A.
    apply/eqP; rewrite -defA eqEsubset OhmS /=; last first.
      rewrite pcore_sub_Hall ?(pHall_subl _ _ sylP) ?joing_subr //.
      exact: subset_trans (pHall_sub hallKP) sEM.
    rewrite -Ohm_id defA OhmS // pcore_max // /normal join_subG.
    rewrite (subset_trans sAP) ?joing_subr // cents_norm 1?centsC //=.
    by rewrite -defA gFnorm.
  have nMsE: E \subset 'N(Ms) by rewrite (subset_trans sEM) ?gFnorm.
  have tiMsE: Ms :&: E = 1.
    by rewrite coprime_TIg ?(pnat_coprime (pcore_pgroup _ _)).
  have <-: Ms * E = M.
    apply/eqP; rewrite eqEcard mulG_subG pcore_sub sEM /= TI_cardMg //.
    by rewrite (card_Hall hallE) (card_Hall (Msigma_Hall maxM)) ?partnC.
  rewrite norm_joinEr -?quotientK ?(subset_trans sAE) //= cosetpre_normal.
  by rewrite quotient_normal // -defA !gFnormal_trans.
pose q := pdiv #|K : 'C_K(A)|.
have q_pr: prime q by rewrite pdiv_prime // indexg_gt1 subsetI subxx centsC.
have [nKA coKA] := (subset_trans sAP nKP, coprimegS sAP coKP).
have [Q sylQ nQA]: exists2 Q : {group gT}, q.-Sylow(K) Q & A \subset 'N(Q).
  by apply: sol_coprime_Sylow_exists => //; apply: (pgroup_sol pA).
have [sQK qQ q'iQK] := and3P sylQ; have [sKE tauK _]:= and3P hallK.
have{q'iQK} not_cQA: ~~ (A \subset 'C(Q)).
  apply: contraL q'iQK => cQA; rewrite p'natE // negbK.
  rewrite -(Lagrange_index (subsetIl K 'C(A))) ?dvdn_mulr ?pdiv_dvd //.
  by rewrite subsetI sQK centsC.
have ntQ: Q :!=: 1 by apply: contraNneq not_cQA => ->; apply: cents1.
have q_dv_K: q %| #|K| := dvdn_trans (pdiv_dvd _) (dvdn_indexg _ _).
have sM'q: q \in (\sigma(M))^' := pgroupP (pgroupS sKE s'E) q q_pr q_dv_K.
have{q_dv_K} tau_q: q \in tau := pgroupP tauK q q_pr q_dv_K.
have sylQ_E: q.-Sylow(E) Q := subHall_Sylow hallK tau_q sylQ.
have sylQ_M: q.-Sylow(M) Q := subHall_Sylow hallE sM'q sylQ_E.
have q'p: p != q by rewrite neq_ltn [p < q]tau_q.
suffices nregQ: 'C_Q(A) != 1.
  have ncycQ: ~~ cyclic Q.
    apply: contra not_cQA => cycQ.
    rewrite (coprime_odd_faithful_Ohm1 qQ) ?mFT_odd ?(coprimeSg sQK) //.
    rewrite centsC; apply: contraR nregQ => not_sQ1_CA.
    rewrite setIC TI_Ohm1 // setIC prime_TIg //.
    by rewrite (Ohm1_cyclic_pgroup_prime cycQ qQ ntQ).
  have {ncycQ} rQ: 'r_q(Q) = 2.
    apply/eqP; rewrite eqn_leq ltnNge -odd_pgroup_rank1_cyclic ?mFT_odd //.
    by rewrite -rE  -rank_pgroup ?rankS // (pHall_sub sylQ_E).
  have [B Eq2B]: exists B, B \in 'E_q^2(Q) by apply/p_rank_geP; rewrite rQ.
  have maxB: B \in 'E*_q(G).
    apply: subsetP (subsetP (pnElemS q 2 (pHall_sub sylQ_M)) B Eq2B).
    by rewrite sigma'_rank2_max // -(p_rank_Sylow sylQ_M).
  have CAq: q %| #|'C(A)|.
    apply: dvdn_trans (cardSg (subsetIr Q _)).
    by have [_ ? _] := pgroup_pdiv (pgroupS (subsetIl Q _) qQ) nregQ.
  have [Qstar maxQstar sQ_Qstar] := max_normed_exists qQ nQA.
  have [|Qm] := max_normed_2Elem_signaliser q'p _ maxQstar CAq.
    by rewrite inE (subsetP (pnElemS p 2 (subsetT M))).
  case=> _ sAQm [_ _ cQstarQm]; rewrite (centSS sAQm sQ_Qstar) // in not_cQA.
  apply: cQstarQm; apply/implyP=> _; apply/set0Pn; exists B.
  have{Eq2B} Eq2B := subsetP (pnElemS q 2 sQ_Qstar) B Eq2B.
  rewrite inE Eq2B (subsetP (pmaxElemS q (subsetT _))) // inE maxB inE.
  by have [? _ _] := pnElemP Eq2B.
pose Q0 := 'Z(Q); have sQ0Q: Q0 \subset Q by apply: gFsub.
have nQ0A: A \subset 'N(Q0) by apply: gFnorm_trans.
have ntQ0: Q0 != 1 by apply: contraNneq ntQ => /(trivg_center_pgroup qQ)->.
apply: contraNneq (sM'q) => regQ; apply/exists_inP; exists Q => //.
suffices nsQ0M: Q0 <| M by rewrite -(mmax_normal _ nsQ0M) ?gFnorms.
have sQ0M: Q0 \subset M := subset_trans sQ0Q (pHall_sub sylQ_M).
have qQ0: q.-group Q0 := pgroupS sQ0Q qQ.
have p'Q0: p^'.-group Q0 by apply: (pi_pnat qQ0); rewrite eq_sym in q'p.
have sM'Q0: \sigma(M)^'.-group Q0 := pi_pnat qQ0 sM'q.
have cQ0Q0: abelian Q0 := center_abelian Q.
have defQ0: [~: A, Q0] = Q0. 
  rewrite -{2}[Q0](coprime_abelian_cent_dprod nQ0A) //.
    by rewrite setIAC regQ setI1g dprodg1 commGC.
  by rewrite (coprimeSg (subset_trans sQ0Q sQK)).
have [_ _ [A1 EpA1 [A2 EpA2 [neqA12 regA1 regA2]]]] := exceptional_structure.
have defA: A1 \x A2 = A by apply/(p2Elem_dprodP Ep2A EpA1 EpA2).
have{defQ0} defQ0: [~: A1, Q0] * [~: A2, Q0] = Q0.
  have{defA} [[_ defA cA12 _] [sA2A _ _]] := (dprodP defA, pnElemP EpA2).
  by rewrite -commMG ?defA // normsR ?(cents_norm cA12) // (subset_trans sA2A).
have sA_NQ0: A \subset 'N_M(Q0) by rewrite subsetI sAM.
have sEpA_EpN := subsetP (pnElemS p 1 sA_NQ0).
have nsRQ0 := commG_sigma'_1Elem_cyclic maxM sQ0M sM'Q0 sM'p (sEpA_EpN _ _).
rewrite -defQ0 -!(commGC Q0).
by apply: normalM; [case/nsRQ0: EpA1 | case/nsRQ0: EpA2].
Qed.

End Section11.