move odd_order to its own repository

1 files changed, 0 insertions, 401 deletions

diff --git a/mathcomp/odd_order/BGsection8.v b/mathcomp/odd_order/BGsection8.v
deleted file mode 100644
index 513d6d1..0000000
--- a/mathcomp/odd_order/BGsection8.v
+++ /dev/null
@@ -1,401 +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 fintype path.
-From mathcomp
-Require Import finset prime fingroup automorphism action gproduct gfunctor.
-From mathcomp
-Require Import center commutator pgroup gseries nilpotent sylow abelian maximal.
-From mathcomp
-Require Import BGsection1 BGsection5 BGsection6 BGsection7.
-
-(******************************************************************************)
-(*   This file covers B & G, section 8, i.e., the proof of two special cases  *)
-(* of the Uniqueness Theorem, for maximal groups with Fitting subgroups of    *)
-(* rank at least 3.                                                           *)
-(******************************************************************************)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Import GroupScope.
-
-Section Eight.
-
-Variable gT : minSimpleOddGroupType.
-Local Notation G := (TheMinSimpleOddGroup gT).
-Implicit Types H M A X P : {group gT}.
-Implicit Types p q r : nat.
-
-Local Notation "K ` p" := 'O_(nat_pred_of_nat p)(K)
-  (at level 8, p at level 2, format "K ` p") : group_scope.
-Local Notation "K ` p" := 'O_(nat_pred_of_nat p)(K)%G : Group_scope.
-
-(* This is B & G, Theorem 8.1(a). *)
-Theorem non_pcore_Fitting_Uniqueness p M A0 :
-    M \in 'M -> ~~ p.-group ('F(M)) -> A0 \in 'E*_p('F(M)) -> 'r_p(A0) >= 3 ->
-  'C_('F(M))(A0)%G \in 'U.
-Proof.
-set F := 'F(M) => maxM p'F /pmaxElemP[/=/setIdP[sA0F abelA0] maxA0].
-have [pA0 cA0A0 _] := and3P abelA0; rewrite (p_rank_abelem abelA0) => dimA0_3.
-rewrite (uniq_mmax_subset1 maxM) //= -/F; last by rewrite subIset ?Fitting_sub.
-set A := 'C_F(A0); pose pi := \pi(A).
-have [sZA sAF]: 'Z(F) \subset A /\ A \subset F by rewrite subsetIl setIS ?centS.
-have nilF: nilpotent F := Fitting_nil _.
-have nilZ := nilpotentS (center_sub _) nilF.
-have piZ: \pi('Z(F)) = \pi(F) by rewrite pi_center_nilpotent.
-have def_pi: pi = \pi(F).
-  by apply/eq_piP=> q; apply/idP/idP; last rewrite -piZ; apply: piSg.
-have def_nZq: forall q, q \in pi -> 'N('Z(F)`q) = M.
-  move=> q; rewrite def_pi -piZ -p_part_gt1.
-  rewrite -(card_Hall (nilpotent_pcore_Hall _ nilZ)) cardG_gt1 /= -/F => ntZ.
-  by apply: mmax_normal => //=; rewrite !gFnormal_trans.
-have sCqM: forall q, q \in pi -> 'C(A`q) \subset M.
-  move=> q /def_nZq <-; rewrite cents_norm // centS //.
-  rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ _)) ?pcore_pgroup //.
-    by apply: nilpotentS (Fitting_nil M); apply: subsetIl.
-  exact: gFsub_trans.
-have sA0A: A0 \subset A by rewrite subsetI sA0F.
-have pi_p: p \in pi.
-  by apply: (piSg sA0A); rewrite -[p \in _]logn_gt0 (leq_trans _ dimA0_3).
-have sCAM: 'C(A) \subset M.
-  by rewrite (subset_trans (centS (pcore_sub p _))) ?sCqM.
-have prM: M \proper G := mmax_proper maxM; have solM := mFT_sol prM.
-have piCA: pi.-group('C(A)).
-  apply/pgroupP=> q q_pr; case/Cauchy=> // x cAx oxq; apply/idPn=> pi'q.
-  have Mx := subsetP sCAM x cAx; pose C := 'C_F(<[x]>).
-  have sAC: A \subset C by rewrite subsetI sAF centsC cycle_subG.
-  have sCFC_C: 'C_F(C) \subset C.
-    by rewrite (subset_trans _ sAC) ?setIS // centS ?(subset_trans _ sAC).
-  have cFx: x \in 'C_M(F).
-    rewrite inE Mx -cycle_subG coprime_nil_faithful_cent_stab //=.
-      by rewrite cycle_subG (subsetP (gFnorm _ _)).
-    by rewrite -orderE coprime_pi' ?cardG_gt0 // -def_pi oxq pnatE.
-  case/negP: pi'q; rewrite def_pi mem_primes q_pr cardG_gt0 -oxq cardSg //.
-  by rewrite cycle_subG (subsetP (cent_sub_Fitting _)).
-have{p'F} pi_alt q: exists2 r, r \in pi & r != q.
-  have [<-{q} | ] := eqVneq p q; last by exists p.
-  rewrite def_pi; apply/allPn; apply: contra p'F => /allP/=pF.
-  by apply/pgroupP=> q q_pr qF; rewrite !inE pF // mem_primes q_pr cardG_gt0.
-have sNZqXq' q X:
-  A \subset X -> X \proper G -> 'O_q^'('N_X('Z(F)`q)) \subset 'O_q^'(X).
-- move=> sAX prX.
-  have sZqX: 'Z(F)`q \subset X by apply: gFsub_trans (subset_trans sZA sAX).
-  have cZqNXZ: 'O_q^'('N_X('Z(F)`q)) \subset 'C('Z(F)`q).
-    have coNq'Zq: coprime #|'O_q^'('N_X('Z(F)`q))| #|'Z(F)`q|.
-      by rewrite coprime_sym coprime_pcoreC.
-    rewrite (sameP commG1P trivgP) -(coprime_TIg coNq'Zq) subsetI commg_subl /=.
-    rewrite commg_subr /= andbC gFsub_trans ?subsetIr //=.
-    by rewrite gFnorm_trans ?normsG // subsetI sZqX normG.
-  have: 'O_q^'('C_X(('Z(F))`q)) \subset 'O_q^'(X).
-    by rewrite p'core_cent_pgroup ?mFT_sol // /psubgroup sZqX pcore_pgroup.
-  apply: subset_trans; apply: subset_trans (pcoreS _ (subcent_sub _ _)).
-  by rewrite !subsetI subxx cZqNXZ gFsub_trans ?subsetIl.
-have sArXq' q r X:
-  q \in pi -> q != r -> A \subset X -> X \proper G -> A`r \subset 'O_q^'(X).
-- move=> pi_q r'q sAX prX; apply: subset_trans (sNZqXq' q X sAX prX).
-  apply: subset_trans (pcoreS _ (subsetIr _ _)).
-  rewrite -setIA (setIidPr (pcore_sub _ _)) subsetI gFsub_trans //= def_nZq //.
-  apply: subset_trans (pcore_Fitting _ _); rewrite -/F.
-  rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ nilF)) ?gFsub_trans //.
-  by apply: (pi_pnat (pcore_pgroup _ _)); rewrite !inE eq_sym.
-have cstrA: normed_constrained A.
-  split=> [||X Y sAX prX].
-  - by apply/eqP=> A1; rewrite /pi /= A1 cards1 in pi_p.
-  - exact: sub_proper_trans (subset_trans sAF (Fitting_sub _)) prM.
-  rewrite !inE -/pi -andbA => /and3P[sYX pi'Y nYA].
-  rewrite -bigcap_p'core subsetI sYX; apply/bigcapsP=> [[q /= _] pi_q].
-  have [r pi_r q'r] := pi_alt q.
-  have{sArXq'} sArXq': A`r \subset 'O_q^'(X) by apply: sArXq'; rewrite 1?eq_sym.
-  have cA_CYr: 'C_Y(A`r) \subset 'C(A).
-    have coYF: coprime #|Y| #|F|.
-      by rewrite coprime_sym coprime_pi' ?cardG_gt0 // -def_pi.
-    rewrite (sameP commG1P trivgP) -(coprime_TIg coYF) commg_subI //.
-      by rewrite setIS // (subset_trans (sCqM r pi_r)) // gFnorm.
-    by rewrite subsetI subsetIl.
-  have{cA_CYr} CYr1: 'C_Y(A`r) = 1.
-    rewrite -(setIid Y) setIAC coprime_TIg // (coprimeSg cA_CYr) //.
-    by rewrite (pnat_coprime piCA).
-  have{CYr1} ->: Y :=: [~: Y, A`r].
-    rewrite -(mulg1 [~: Y, _]) -CYr1 coprime_cent_prod ?gFsub_trans //.
-      rewrite coprime_sym (coprimeSg (pcore_sub _ _)) //= -/A.
-      by rewrite coprime_pi' ?cardG_gt0.
-    by rewrite mFT_sol // (sub_proper_trans sYX).
-  rewrite (subset_trans (commgS _ sArXq')) //.
-  by rewrite commg_subr gFnorm_trans ?normsG.
-have{cstrA} nbyApi'1 q: q \in pi^' -> |/|*(A; q) = [set 1%G].
-  move=> pi'q; have trA: [transitive 'O_pi^'('C(A)), on |/|*(A; q) | 'JG].
-    apply: normed_constrained_rank3_trans; rewrite //= -/A.
-    rewrite -rank_abelem // in dimA0_3; apply: leq_trans dimA0_3 (rankS _).
-    by rewrite /= -/A subsetI sA0A centsC subsetIr.
-  have [Q maxQ defAmax]: exists2 Q, Q \in |/|*(A; q) & |/|*(A; q) = [set Q].
-    case/imsetP: trA => Q maxQ defAmax; exists Q; rewrite // {maxQ}defAmax.
-    suffices ->: 'O_pi^'('C(A)) = 1 by rewrite /orbit imset_set1 act1.
-    rewrite -(setIidPr (pcore_sub _ _)) coprime_TIg //.
-    exact: pnat_coprime piCA (pcore_pgroup _ _).
-  have{maxQ} qQ: q.-group Q by move: maxQ; rewrite inE => /maxgroupp/andP[].
-  have [<- // |] := eqVneq Q 1%G; rewrite -val_eqE /= => ntQ.
-  have{defAmax trA} defFmax: |/|*(F; q) = [set Q].
-    apply/eqP; rewrite eqEcard cards1 -defAmax.
-    have snAF: A <|<| F by rewrite nilpotent_subnormal ?Fitting_nil.
-    have piF: pi.-group F by rewrite def_pi /pgroup pnat_pi ?cardG_gt0.
-    case/(normed_trans_superset _ _ snAF): trA => //= _ /imsetP[R maxR _] -> _.
-    by rewrite (cardsD1 R) maxR.
-  have nQM: M \subset 'N(Q).
-    apply/normsP=> x Mx; apply: congr_group; apply/set1P.
-    rewrite -defFmax (acts_act (norm_acts_max_norm _ _)) ?defFmax ?set11 //.
-    by apply: subsetP Mx; apply: gFnorm.
-  have{nQM} nsQM: Q <| M.
-    rewrite inE in maxM; case/maxgroupP: maxM => _ maxM.
-    rewrite -(maxM 'N(Q)%G) ?normalG ?mFT_norm_proper //.
-    exact: mFT_pgroup_proper qQ.
-  have sQF: Q \subset F by rewrite Fitting_max ?(pgroup_nil qQ).
-  rewrite -(setIidPr sQF) coprime_TIg ?eqxx // in ntQ.
-  by rewrite coprime_pi' ?cardG_gt0 // -def_pi (pi_pnat qQ).
-apply/subsetP=> H /setIdP[maxH sAH]; rewrite inE -val_eqE /=.
-have prH: H \proper G := mmax_proper maxH; have solH := mFT_sol prH.
-pose D := 'F(H); have nilD: nilpotent D := Fitting_nil H.
-have card_pcore_nil := card_Hall (nilpotent_pcore_Hall _ _).
-have piD: \pi(D) = pi.
-  set sigma := \pi(_); have pi_sig: {subset sigma <= pi}.
-    move=> q; rewrite -p_part_gt1 -card_pcore_nil // cardG_gt1 /= -/D.
-    apply: contraR => /nbyApi'1 defAmax.
-    have nDqA: A \subset 'N(D`q).
-      by rewrite gFnorm_trans // (subset_trans sAH) ?gFnorm.
-    have [Q]:= max_normed_exists (pcore_pgroup _ _) nDqA.
-    by rewrite defAmax -subG1; move/set1P->.
-  apply/eq_piP=> q; apply/idP/idP=> [|pi_q]; first exact: pi_sig.
-  apply: contraLR (pi_q) => sig'q; have nilA := nilpotentS sAF nilF.
-  rewrite -p_part_eq1 -card_pcore_nil // -trivg_card1 -subG1 /= -/A.
-  have <-: 'O_sigma^'(H) = 1.
-    apply/eqP; rewrite -trivg_Fitting ?(solvableS (pcore_sub _ _)) //.
-    rewrite Fitting_pcore -(setIidPr (pcore_sub _ _)) coprime_TIg //.
-    by rewrite coprime_pi' ?cardG_gt0 //; apply: pcore_pgroup.
-  rewrite -bigcap_p'core subsetI gFsub_trans //=.
-  apply/bigcapsP=> -[r /= _] sig_r; apply: sArXq' => //; first exact: pi_sig.
-  by apply: contraNneq sig'q => <-.
-have cAD q r: q != r -> D`q \subset 'C(A`r).
-  move=> r'q; have [-> |] := eqVneq D`q 1; first by rewrite sub1G.
-  rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piD => pi_q.
-  have sArHq': A`r \subset 'O_q^'(H) by rewrite sArXq'.
-  have coHqHq': coprime #|D`q| #|'O_q^'(H)| by rewrite coprime_pcoreC.
-  rewrite (sameP commG1P trivgP) -(coprime_TIg coHqHq') commg_subI //.
-    by rewrite subsetI subxx /= p_core_Fitting gFsub_trans ?gFnorm.
-  rewrite subsetI sArHq' gFsub_trans ?(subset_trans sAH) //=.
-  by rewrite p_core_Fitting gFnorm.
-have sDM: D \subset M.
-  rewrite [D]FittingEgen gen_subG; apply/bigcupsP=> [[q /= _] _].
-  rewrite -p_core_Fitting -/D; have [r pi_r r'q] := pi_alt q.
-  by apply: subset_trans (sCqM r pi_r); apply: cAD; rewrite eq_sym.
-have cApHp': A`p \subset 'C('O_p^'(H)).
-  have coApHp': coprime #|'O_p^'(H)| #|A`p|.
-    by rewrite coprime_sym coprime_pcoreC.
-  have solHp': solvable 'O_p^'(H) by rewrite (solvableS (pcore_sub _ _)).
-  have nHp'Ap: A`p \subset 'N('O_p^'(H)).
-    by rewrite gFsub_trans ?gFnorm_trans ?normsG.
-  apply: subset_trans (coprime_cent_Fitting nHp'Ap coApHp' solHp').
-  rewrite subsetI subxx centsC /= FittingEgen gen_subG.
-  apply/bigcupsP=> [[q /= _] _]; have [-> | /cAD] := eqVneq q p.
-    by rewrite -(setIidPl (pcore_sub p _)) TI_pcoreC sub1G.
-  apply: subset_trans; rewrite p_core_Fitting -pcoreI.
-  by apply: sub_pcore => r /andP[].
-have sHp'M: 'O_p^'(H) \subset M.
-  by apply: subset_trans (sCqM p pi_p); rewrite centsC.
-have ntDp: D`p != 1 by rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piD.
-have sHp'_NMDp': 'O_p^'(H) \subset 'O_p^'('N_M(D`p)).
-  apply: subset_trans (pcoreS _ (subsetIr _ _)).
-  rewrite -setIA (setIidPr (pcore_sub _ _)) /= (mmax_normal maxH) //.
-    by rewrite subsetI sHp'M subxx.
-  by rewrite /= p_core_Fitting pcore_normal.
-have{sHp'_NMDp'} sHp'Mp': 'O_p^'(H) \subset 'O_p^'(M).
-  have pM_D: p.-subgroup(M) D`p.
-    by rewrite /psubgroup pcore_pgroup gFsub_trans.
-  apply: subset_trans (p'core_cent_pgroup pM_D (mFT_sol prM)).
-  apply: subset_trans (pcoreS _ (subcent_sub _ _)).
-  rewrite !subsetI sHp'_NMDp' sHp'M andbT /= (sameP commG1P trivgP).
-  have coHp'Dp: coprime #|'O_p^'(H)| #|D`p|.
-    by rewrite coprime_sym coprime_pcoreC.
-  rewrite -(coprime_TIg coHp'Dp) subsetI commg_subl commg_subr /=.
-  by rewrite p_core_Fitting !gFsub_trans ?gFnorm.
-have sMp'H: 'O_p^'(M) \subset H.
-  rewrite -(mmax_normal maxH (pcore_normal p H)) /= -p_core_Fitting //.
-  rewrite -/D (subset_trans _ (cent_sub _)) // centsC.
-  have solMp' := solvableS (pcore_sub p^' _) (mFT_sol prM).
-  have coMp'Dp: coprime #|'O_p^'(M)| #|D`p|.
-    by rewrite coprime_sym coprime_pcoreC.
-  have nMp'Dp: D`p \subset 'N('O_p^'(M)).
-    by rewrite gFsub_trans ?(subset_trans sDM) ?gFnorm.
-  apply: subset_trans (coprime_cent_Fitting nMp'Dp coMp'Dp solMp').
-  rewrite subsetI subxx centsC /= FittingEgen gen_subG.
-  apply/bigcupsP=> [[q /= _] _]; have [<- | /cAD] := eqVneq p q.
-    by rewrite -(setIidPl (pcore_sub p _)) TI_pcoreC sub1G.
-  rewrite centsC; apply: subset_trans.
-  rewrite -p_core_Fitting Fitting_pcore pcore_max ?pcore_pgroup //=.
-  rewrite /normal subsetI -pcoreI pcore_sub subIset ?gFnorm //=.
-  rewrite pcoreI gFsub_trans //= -/F centsC.
-  case/dprodP: (nilpotent_pcoreC p nilF) => _ _ /= cFpp' _.
-  rewrite centsC (subset_trans cFpp' (centS _)) //.
-  have hallFp := nilpotent_pcore_Hall p nilF.
-  by rewrite (sub_Hall_pcore hallFp).
-have{sHp'Mp' sMp'H} eqHp'Mp': 'O_p^'(H) = 'O_p^'(M).
-  apply/eqP; rewrite eqEsubset sHp'Mp'.
-  apply: subset_trans (sNZqXq' p H sAH prH).
-  apply: subset_trans (pcoreS _ (subsetIr _ _)).
-  rewrite -setIA (setIidPr (pcore_sub _ _)) subsetI sMp'H /=.
-  rewrite (mmax_normal maxM) ?gFnormal_trans //.
-  by rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piZ -def_pi.
-have ntHp': 'O_p^'(H) != 1.
-  have [q pi_q p'q] := pi_alt p; have: D`q \subset 'O_p^'(H).
-    by rewrite p_core_Fitting sub_pcore // => r; move/eqnP->.
-  rewrite -proper1G; apply: proper_sub_trans; rewrite proper1G.
-  by rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piD.
-rewrite -(mmax_normal maxH (pcore_normal p^' H)) //= eqHp'Mp'.
-by rewrite (mmax_normal maxM (pcore_normal _ _)) //= -eqHp'Mp'.
-Qed.
-
-(* This is B & G, Theorem 8.1(b). *)
-Theorem SCN_Fitting_Uniqueness p M P A :
-    M \in 'M -> p.-group ('F(M)) -> p.-Sylow(M) P ->
-    'r_p('F(M)) >= 3 -> A \in 'SCN_3(P) ->
-  [/\ p.-Sylow(G) P, A \subset 'F(M) & A \in 'U].
-Proof.
-set F := 'F(M) => maxM pF sylP dimFp3 scn3_A.
-have [scnA dimA3] := setIdP scn3_A; have [nsAP defCA] := SCN_P scnA.
-have cAA := SCN_abelian scnA; have sAP := normal_sub nsAP.
-have [sPM pP _] := and3P sylP; have sAM := subset_trans sAP sPM.
-have{dimA3} ntA: A :!=: 1 by case: eqP dimA3 => // ->; rewrite rank1.
-have prM := mmax_proper maxM; have solM := mFT_sol prM.
-have{pF} Mp'1: 'O_p^'(M) = 1.
-  apply/eqP; rewrite -trivg_Fitting ?(solvableS (pcore_sub _ _)) //.
-  rewrite Fitting_pcore -(setIidPr (pcore_sub _ _)) coprime_TIg //.
-  exact: pnat_coprime (pcore_pgroup _ _).
-have defF: F = M`p := Fitting_eq_pcore Mp'1.
-have sFP: F \subset P by rewrite defF (pcore_sub_Hall sylP).
-have sAF: A \subset F.
-  rewrite defF -(pseries_pop2 _ Mp'1).
-  exact: (odd_p_abelian_constrained (mFT_odd _) solM sylP cAA nsAP).
-have sZA: 'Z(F) \subset A.
-  by rewrite -defCA setISS ?centS // defF pcore_sub_Hall.
-have sCAM: 'C(A) \subset M.
-  have nsZM: 'Z(F) <| M by rewrite !gFnormal_trans.
-  rewrite -(mmax_normal maxM nsZM); last first.
-    rewrite /= -(setIidPr (center_sub _)) meet_center_nil ?Fitting_nil //.
-    by rewrite -proper1G (proper_sub_trans _ sAF) ?proper1G.
-  by rewrite (subset_trans _ (cent_sub _)) ?centS.
-have nsZL_M: 'Z('L(P)) <| M.
-  by rewrite (Puig_center_normal (mFT_odd _) solM sylP).
-have sNPM: 'N(P) \subset M.
-  rewrite -(mmax_normal maxM nsZL_M) ?gFnorm_trans //.
-  apply/eqP => /(trivg_center_Puig_pgroup (pHall_pgroup sylP))-P1.
-  by rewrite -subG1 -P1 sAP in ntA.
-have sylPG: p.-Sylow(G) P := mmax_sigma_Sylow maxM sylP sNPM.
-split; rewrite // (uniq_mmax_subset1 maxM sAM).
-have{scn3_A} scn3_A: A \in 'SCN_3[p] by apply/bigcupP; exists P; rewrite // inE.
-pose K := 'O_p^'('C(A)); have sKF: K \subset F.
-  have sKM: K \subset M := gFsub_trans _ sCAM.
-  apply: subset_trans (cent_sub_Fitting solM).
-  rewrite subsetI sKM coprime_nil_faithful_cent_stab ?Fitting_nil //.
-  - by rewrite gFsub_trans ?(subset_trans sCAM) ?gFnorm.
-  - by rewrite /= -/F defF coprime_pcoreC.
-  have sACK: A \subset 'C_F(K) by rewrite subsetI sAF centsC pcore_sub.
-  by rewrite /= -/F -/K (subset_trans _ sACK) //= -defCA setISS ?centS.
-have{sKF} K1: K = 1 by rewrite -(setIidPr sKF) defF TI_pcoreC.
-have p'nbyA_1 q: q != p -> |/|*(A; q) = [set 1%G].
-  move=> p'q.
-  have: [transitive K, on |/|*(A; q) | 'JG] by apply: Thompson_transitivity.
-  case/imsetP=> Q maxQ; rewrite K1 /orbit imset_set1 act1 => defAmax.
-  have nQNA: 'N(A) \subset 'N(Q).
-    apply/normsP=> x Nx; apply: congr_group; apply/set1P; rewrite -defAmax.
-    by rewrite (acts_act (norm_acts_max_norm _ _)).
-  have{nQNA} nQF: F \subset 'N(Q).
-    exact: subset_trans (subset_trans (normal_norm nsAP) nQNA).
-  have defFmax: |/|*(F; q) = [set Q] := max_normed_uniq defAmax sAF nQF.
-  have nQM: M \subset 'N(Q).
-    apply/normsP=> x Mx; apply: congr_group; apply/set1P; rewrite -defFmax.
-    rewrite (acts_act (norm_acts_max_norm _ _)) ?defFmax ?set11 //.
-    by rewrite (subsetP (gFnorm _ _)).
-  have [<- // | ntQ] := eqVneq Q 1%G.
-  rewrite inE in maxQ; have [qQ _] := andP (maxgroupp maxQ).
-  have{nQM} defNQ: 'N(Q) = M.
-    by rewrite (mmax_norm maxM) // (mFT_pgroup_proper qQ).
-  case/negP: ntQ; rewrite -[_ == _]subG1 -Mp'1 -defNQ pcore_max ?normalG //.
-  exact: pi_pnat qQ _.
-have{p'nbyA_1} p'nbyA_1 X:
-  X \proper G -> p^'.-group X -> A \subset 'N(X) -> X :=: 1.
-- move=> prX p'X nXA; have solX := mFT_sol prX.
-  apply/eqP; rewrite -trivg_Fitting // -subG1 /= FittingEgen gen_subG.
-  apply/bigcupsP=> [[q /= _] _]; have [-> | p'q] := eqVneq q p.
-    rewrite -(setIidPl (pcore_sub _ _)) coprime_TIg //.
-    by rewrite (pnat_coprime (pcore_pgroup _ _)).
-  have [R] := max_normed_exists (pcore_pgroup q X) (gFnorm_trans _ nXA).
-  by rewrite p'nbyA_1 // => /set1P->.
-apply/subsetPn=> -[H0 MA_H0 neH0M].
-pose H := [arg max_(H > H0 | (H \in 'M(A)) && (H != M)) #|H :&: M|`_p].
-case: arg_maxP @H => [|H {H0 MA_H0 neH0M}]; first by rewrite MA_H0 -in_set1.
-rewrite /= inE -andbA => /and3P[maxH sAH neHM] maxHM.
-have prH: H \proper G by rewrite inE in maxH; apply: maxgroupp maxH.
-have sAHM: A \subset H :&: M by rewrite subsetI sAH.
-have [R sylR_HM sAR]:= Sylow_superset sAHM (pgroupS sAP pP).
-have [/subsetIP[sRH sRM] pR _] := and3P sylR_HM.
-have{sylR_HM} sylR_H: p.-Sylow(H) R.
-  have [Q sylQ] := Sylow_superset sRM pR; have [sQM pQ _] := and3P sylQ.
-  case/eqVproper=> [defR | /(nilpotent_proper_norm (pgroup_nil pQ)) sRN].
-    apply: (pHall_subl sRH (subsetT _)); rewrite pHallE subsetT /=.
-    by rewrite -(card_Hall sylPG) (card_Hall sylP) defR (card_Hall sylQ).
-  case/maximal_exists: (subsetT 'N(R)) => [nRG | [D maxD sND]].
-    case/negP: (proper_irrefl (mem G)); rewrite -{1}nRG.
-    rewrite mFT_norm_proper ?(mFT_pgroup_proper pR) //.
-    by rewrite -proper1G (proper_sub_trans _ sAR) ?proper1G.
-  move/implyP: (maxHM D); rewrite 2!inE {}maxD leqNgt.
-  case: eqP sND => [->{D} sNM _ | _ sND].
-    rewrite -Sylow_subnorm (pHall_subl _ _ sylR_HM) ?setIS //.
-    by rewrite subsetI sRH normG.
-  rewrite (subset_trans (subset_trans sAR (normG R)) sND); case/negP.
-  rewrite -(card_Hall sylR_HM) (leq_trans (proper_card sRN)) //.
-  rewrite -(part_pnat_id (pgroupS (subsetIl _ _) pQ)) dvdn_leq //.
-  by rewrite partn_dvd ?cardG_gt0 // cardSg //= setIC setISS.
-have Hp'1: 'O_p^'(H) = 1.
-  apply: p'nbyA_1 (pcore_pgroup _ _) (subset_trans sAH (gFnorm _ _)).
-  exact: sub_proper_trans (pcore_sub _ _) prH.
-have nsZLR_H: 'Z('L(R)) <| H.
-  exact: Puig_center_normal (mFT_odd _) (mFT_sol prH) sylR_H _.
-have ntZLR: 'Z('L(R)) != 1.
-  apply/eqP=> /(trivg_center_Puig_pgroup pR) R1.
-  by rewrite -subG1 -R1 sAR in ntA.
-have defH: 'N('Z('L(R))) = H := mmax_normal maxH nsZLR_H ntZLR.
-have{sylR_H} sylR: p.-Sylow(G) R.
-  rewrite -Sylow_subnorm setTI (pHall_subl _ _ sylR_H) ?normG //=.
-  by rewrite -defH !gFnorm_trans.
-have nsZLR_M: 'Z('L(R)) <| M.
-  have sylR_M := pHall_subl sRM (subsetT _) sylR.
-  exact: Puig_center_normal (mFT_odd _) solM sylR_M _.
-case/eqP: neHM; apply: group_inj.
-by rewrite -defH (mmax_normal maxM nsZLR_M).
-Qed.
-
-(* This summarizes the two branches of B & G, Theorem 8.1. *)
-Theorem Fitting_Uniqueness M : M \in 'M -> 'r('F(M)) >= 3 -> 'F(M)%G \in 'U.
-Proof.
-move=> maxM; have [p _ -> dimF3] := rank_witness 'F(M).
-have prF: 'F(M) \proper G := sub_mmax_proper maxM (Fitting_sub M).
-have [pF | npF] := boolP (p.-group 'F(M)).
-  have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP.
-  have dimP3: 'r_p(P) >= 3.
-    rewrite (p_rank_Sylow sylP) (leq_trans dimF3) //.
-    by rewrite p_rankS ?Fitting_sub.
-  have [A] := rank3_SCN3 pP (mFT_odd _) dimP3.
-  by case/(SCN_Fitting_Uniqueness maxM pF)=> // _ sAF; apply: uniq_mmaxS.
-case/p_rank_geP: dimF3 => A /setIdP[EpA dimA3].
-have [A0 maxA0 sAA0] := @maxgroup_exists _ [pred X in 'E_p('F(M))] _ EpA.
-have [_ abelA] := pElemP EpA; have pmaxA0: A0 \in 'E*_p('F(M)) by rewrite inE.
-case/pElemP: (maxgroupp maxA0) => sA0F; case/and3P=> _ cA0A0 _.
-have dimA0_3: 'r_p(A0) >= 3.
-  by rewrite -(eqP dimA3) -(p_rank_abelem abelA) p_rankS.
-have:= non_pcore_Fitting_Uniqueness maxM npF pmaxA0 dimA0_3.
-exact: uniq_mmaxS (subsetIl _ _) prF.
-Qed.
-
-End Eight.
-