Timings for BGsection1.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 path div fintype.
From mathcomp
Require Import bigop prime binomial finset fingroup morphism perm automorphism.
From mathcomp
Require Import quotient action gproduct gfunctor commutator.
From mathcomp
Require Import ssralg finalg zmodp cyclic center pgroup finmodule gseries.
From mathcomp
Require Import nilpotent sylow abelian maximal hall extremal.
From mathcomp
Require Import matrix mxalgebra mxrepresentation mxabelem.

(******************************************************************************)
(* This file contains most of the material in B & G, section 1, including the *)
(* definitions:                                                               *)
(*         p.-length_1 G == the upper p-series of G has length <= 1, i.e.,    *)
(*                          'O_{p^',p,p^'}(G) = G                             *)
(*         p_elt_gen p G == the subgroup of G generated by its p-elements.    *)
(* This file currently covers B & G 1.3-4, 1.6, 1.8-1.21, and also            *)
(* Gorenstein 8.1.3 and 2.8.1 (maximal order of a p-subgroup of GL(2,p)).     *)
(*   This file also provides, mostly for future reference, the following      *)
(* definitions, drawn from Gorenstein, Chapter 8, and B & G, Appendix B:      *)
(*     p.-constrained G <-> the p',p core of G contains the centralisers of   *)
(*                          all its Sylow p-subgroups. The Hall-Higman Lemma  *)
(*                          1.2.3 (B & G, 1.15a) asserts that this holds for  *)
(*                          all solvable groups.                              *)
(*          p.-stable G <-> a rather group theoretic generalization of the    *)
(*                          Hall-Higman type condition that in a faithful     *)
(*                          p-modular linear representation of G no p-element *)
(*                          has a quadratic minimal polynomial, to groups G   *)
(*                          with a non-trivial p-core.                        *)
(* p.-abelian_constrained <-> the p',p core of G contains all the normal      *)
(*                          abelian subgroups of the Sylow p-subgroups of G.  *)
(*                          It is via this property and the ZL theorem (the   *)
(*                          substitute for the ZJ theorem) that the           *)
(*                          p-stability of groups of odd order is exploited   *)
(*                          in the proof of the Odd Order Theorem.            *)
(*      generated_by p G == G is generated by a set of subgroups satisfying   *)
(*                          p : pred {group gT}                               *)
(*      norm_abelian X A == A is abelian and normalised by X.                 *)
(*  p_norm_abelian p X A == A is an abelian p-group normalised by X.          *)
(*             'L_[G](X) == the group generated by the abelian subgroups of G *)
(*                          normalized by X.                                  *)
(*             'L_{n}(G) == the Puig group series, defined by the recurrence  *)
(*                          'L_{0}(G) = 1, 'L_{n.+1}(G) = 'L_[G]('L_{n}(G)).  *)
(*               'L_*(G) == the lower limit of the Puig series.               *)
(*                 'L(G) == the Puig subgroup: the upper limit of the Puig    *)
(*                          series: 'L(G) = 'L_[G]('L_*(G)) and conversely.   *)
(*  The following notation is used locally here and in AppendixB, but is NOT  *)
(* exported:                                                                  *)
(*               D --> G == G is generated by abelian groups normalised by D  *)
(*                       := generated_by (norm_abelian D) G                   *)
(******************************************************************************)

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

Import GroupScope.

Section Definitions.

Variables (n : nat) (gT : finGroupType).
Implicit Type p : nat.

Definition plength_1 p (G : {set gT}) := 'O_{p^', p, p^'}(G) == G.

Definition p_elt_gen p (G : {set gT}) := <<[set x in G | p.-elt x]>>.

Definition p_constrained p (G : {set gT}) :=
  forall P : {group gT},
    p.-Sylow('O_{p^',p}(G)) P ->
  'C_G(P) \subset 'O_{p^',p}(G).

Definition p_abelian_constrained p (G : {set gT}) :=
  forall S A : {group gT},
    p.-Sylow(G) S -> abelian A -> A <| S ->
  A \subset 'O_{p^',p}(G).

Definition p_stable p (G : {set gT}) :=
  forall P A : {group gT},
     p.-group P -> 'O_p^'(G) * P <| G ->
     p.-subgroup('N_G(P)) A -> [~: P, A, A] = 1 ->
  A / 'C_G(P) \subset 'O_p('N_G(P) / 'C_G(P)).

Definition generated_by (gp : pred {group gT}) (E : {set gT}) :=
  [exists gE : {set {group gT}}, <<\bigcup_(G in gE | gp G) G>> == E].

Definition norm_abelian (D : {set gT}) : pred {group gT} :=
  fun A => (D \subset 'N(A)) && abelian A.

Definition p_norm_abelian p (D : {set gT}) : pred {group gT} :=
  fun A => p.-group A && norm_abelian D A.

Definition Puig_succ (D E : {set gT}) :=
  <<\bigcup_(A in subgroups D | norm_abelian E A) A>>.

Definition Puig_rec D := iter n (Puig_succ D) 1.

End Definitions.

(* This must be defined outside a Section to avoid spurrious delta-reduction *)
Definition Puig_at := nosimpl Puig_rec.

Definition Puig_inf (gT : finGroupType) (G : {set gT}) := Puig_at #|G|.*2 G.

Definition Puig (gT : finGroupType) (G : {set gT}) := Puig_at #|G|.*2.+1 G.

Notation "p .-length_1" := (plength_1 p)
  (at level 2, format "p .-length_1") : group_scope.

Notation "p .-constrained" := (p_constrained p)
  (at level 2, format "p .-constrained") : group_scope.
Notation "p .-abelian_constrained" := (p_abelian_constrained p)
  (at level 2, format "p .-abelian_constrained") : group_scope.
Notation "p .-stable" := (p_stable p)
  (at level 2, format "p .-stable") : group_scope.

Notation "''L_[' G ] ( L )" := (Puig_succ G L)
  (at level 8, format  "''L_[' G ] ( L )") : group_scope.
Notation "''L_{' n } ( G )" := (Puig_at n G)
  (at level 8, format "''L_{' n } ( G )") : group_scope.
Notation "''L_*' ( G )" := (Puig_inf G)
  (at level 8, format "''L_*' ( G )") : group_scope.
Notation "''L' ( G )" := (Puig G)
  (at level 8, format "''L' ( G )") : group_scope.

Section BGsection1.

Implicit Types (gT : finGroupType) (p : nat).

(* This is B & G, Lemma 1.1, first part. *)
Lemma minnormal_solvable_abelem gT (M G : {group gT}) :
  minnormal M G -> solvable M -> is_abelem M.
Proof. by move=> minM solM; case: (minnormal_solvable minM (subxx _) solM). Qed.

(* This is B & G, Lemma 1.2, second part. *)
Lemma minnormal_solvable_Fitting_center gT (M G : {group gT}) :
  minnormal M G ->  M \subset G -> solvable M -> M \subset 'Z('F(G)).
Proof.
have nZG: 'Z('F(G)) <| G by rewrite !gFnormal_trans.
move=> minM sMG solM; have[/andP[ntM nMG] minM'] := mingroupP minM.
apply/setIidPl/minM'; last exact: subsetIl.
apply/andP; split; last by rewrite normsI // normal_norm.
apply: meet_center_nil => //; first by apply: Fitting_nil.
apply/andP; split; last exact: gFsub_trans.
apply: Fitting_max; rewrite // /normal ?sMG //; apply: abelian_nil. 
by move: (minnormal_solvable_abelem minM solM) => /abelem_abelian.
Qed.

Lemma sol_chief_abelem gT (G V U : {group gT}) : 
  solvable G -> chief_factor G V U -> is_abelem (U / V).
Proof.
move=> solG chiefUV; have minUV := chief_factor_minnormal chiefUV.
have [|//] := minnormal_solvable minUV (quotientS _ _) (quotient_sol _ solG).
by case/and3P: chiefUV.
Qed.

Section HallLemma.

Variables (gT : finGroupType) (G G' : {group gT}).

Hypothesis solG : solvable G.
Hypothesis nsG'G : G' <| G.

Let sG'G : G' \subset G. Proof. exact: normal_sub. Qed.
Let nG'G : G \subset 'N(G'). Proof. exact: normal_norm. Qed.
Let nsF'G : 'F(G') <| G. Proof. exact: gFnormal_trans. Qed.

Let Gchief (UV : {group gT} * {group gT}) := chief_factor G UV.2 UV.1.
Let H := \bigcap_(UV | Gchief UV) 'C(UV.1 / UV.2 | 'Q).
Let H' :=
  G' :&: \bigcap_(UV | Gchief UV && (UV.1 \subset 'F(G'))) 'C(UV.1 / UV.2 | 'Q).

(* This is B & G Proposition 1.2, non trivial inclusion of the first equality.*)
Proposition Fitting_stab_chief : 'F(G') \subset H.
Proof.
apply/bigcapsP=> [[U V] /= chiefUV].
have minUV: minnormal (U / V) (G / V) := chief_factor_minnormal chiefUV.
have{chiefUV} [/=/maxgroupp/andP[_ nVG] sUG nUG] := and3P chiefUV.
have solUV: solvable (U / V) by rewrite quotient_sol // (solvableS sUG).
have{solUV minUV}: U / V \subset 'Z('F(G / V)).
  exact: minnormal_solvable_Fitting_center minUV (quotientS V sUG) solUV.
rewrite sub_astabQ gFsub_trans ?(subset_trans sG'G) //=.
case/subsetIP=> _; rewrite centsC; apply: subset_trans.
by rewrite Fitting_max ?quotient_normal ?quotient_nil ?Fitting_nil.
Qed.

(* This is B & G Proposition 1.2, non trivial inclusion of the second         *)
(* equality.                                                                  *)
Proposition chief_stab_sub_Fitting : H' \subset 'F(G').
Proof.
without loss: / {K | [min K | K <| G & ~~ (K \subset 'F(G'))] & K \subset H'}.
  move=> IH; apply: wlog_neg => s'H'F; apply/IH/mingroup_exists=> {IH}/=.
  rewrite /normal subIset ?sG'G ?normsI ?norms_bigcap {s'H'F}//.
  apply/bigcapsP=> /= U /andP[/and3P[/maxgroupp/andP/=[_ nU2G] _ nU1G] _].
  exact: subset_trans (actsQ nU2G nU1G) (astab_norm 'Q (U.1 / U.2)).
case=> K /mingroupP[/andP[nsKG s'KF] minK] /subsetIP[sKG' nFK].
have [[Ks chiefKs defK] sKG]:= (chief_series_exists nsKG, normal_sub nsKG).
suffices{nsKG s'KF} cKsK: (K.-central).-series 1%G Ks.
  by rewrite Fitting_max ?(normalS _ sG'G) ?(centrals_nil cKsK) in s'KF.
move: chiefKs; rewrite -!(rev_path _ _ Ks) {}defK.
case: {Ks}(rev _) => //= K1 Kr /andP[chiefK1 chiefKr].
have [/maxgroupp/andP[/andP[sK1K ltK1K] nK1G] _] := andP chiefK1.
suffices{chiefK1} cKrK: [rel U V | central_factor K V U].-series K1 Kr.
  have cKK1: abelian (K / K1) := abelem_abelian (sol_chief_abelem solG chiefK1).
  by rewrite /central_factor subxx sK1K der1_min //= (subset_trans sKG).
have{minK ltK1K nK1G} sK1F: K1 \subset 'F(G').
  have nsK1G: K1 <| G by rewrite /normal (subset_trans sK1K).
  by apply: contraR ltK1K => s'K1F; rewrite (minK K1) ?nsK1G.
elim: Kr K1 chiefKr => //= K2 Kr IHr K1 /andP[chiefK2 chiefKr] in sK1F sK1K *.
have [/maxgroupp/andP[/andP[sK21 _] /(subset_trans sKG)nK2K] _] := andP chiefK2.
rewrite /central_factor sK1K {}IHr ?(subset_trans sK21) {chiefKr}// !andbT.
rewrite commGC -sub_astabQR ?(subset_trans _ nK2K) //.
exact/(subset_trans nFK)/(bigcap_inf (K1, K2))/andP.
Qed.

End HallLemma.

(* This is B & G, Proposition 1.3 (due to P. Hall). *)
Proposition cent_sub_Fitting gT (G : {group gT}) :
  solvable G -> 'C_G('F(G)) \subset 'F(G).
Proof.
move=> solG; apply: subset_trans (chief_stab_sub_Fitting solG _) => //.
rewrite subsetI subsetIl; apply/bigcapsP=> [[U V]] /=.
case/andP=> /andP[/maxgroupp/andP[_ nVG] _] sUF.
by rewrite astabQ (subset_trans _ (morphpre_cent _ _)) // setISS ?centS.
Qed.

(* This is B & G, Proposition 1.4, for internal actions.                      *)
Proposition coprime_trivg_cent_Fitting gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|G| #|A| -> solvable G -> 
  'C_A(G) = 1 -> 'C_A('F(G)) = 1.
Proof.
move=> nGA coGA solG regAG; without loss cycA: A nGA coGA regAG / cyclic A.
  move=> IH; apply/trivgP/subsetP=> a; rewrite -!cycle_subG subsetI.
  case/andP=> saA /setIidPl <-.
  rewrite {}IH ?cycle_cyclic ?(coprimegS saA) ?(subset_trans saA) //.
  by apply/trivgP; rewrite -regAG setSI.
pose X := G <*> A; pose F := 'F(X); pose pi := \pi(A); pose Q := 'O_pi(F).
have pi'G: pi^'.-group G by rewrite /pgroup -coprime_pi' //= coprime_sym.
have piA: pi.-group A by apply: pgroup_pi.
have oX: #|X| = (#|G| * #|A|)%N by rewrite [X]norm_joinEr ?coprime_cardMg.
have hallG: pi^'.-Hall(X) G.
  by rewrite /pHall -divgS joing_subl //= pi'G pnatNK oX mulKn.
have nsGX: G <| X by rewrite /normal joing_subl join_subG normG.
have{oX pi'G piA} hallA: pi.-Hall(X) A.
  by rewrite /pHall -divgS joing_subr //= piA oX mulnK.
have nsQX: Q <| X by rewrite !gFnormal_trans.
have{solG cycA} solX: solvable X.
  rewrite (series_sol nsGX) {}solG /= norm_joinEr // quotientMidl //.
  by rewrite morphim_sol // abelian_sol // cyclic_abelian.
have sQA: Q \subset A.
  by apply: normal_sub_max_pgroup (Hall_max hallA) (pcore_pgroup _ _) nsQX.
have pi'F: 'O_pi(F) = 1.
  suff cQG: G \subset 'C(Q) by apply/trivgP; rewrite -regAG subsetI sQA centsC.
  apply/commG1P/trivgP; rewrite -(coprime_TIg coGA) subsetI commg_subl.
  rewrite (subset_trans sQA) // (subset_trans _ sQA) // commg_subr.
  by rewrite (subset_trans _ (normal_norm nsQX)) ?joing_subl.
have sFG: F \subset G.
  have /dprodP[_ defF _ _]: _ = F := nilpotent_pcoreC pi (Fitting_nil _).
  by rewrite (sub_normal_Hall hallG) ?gFsub //= -defF pi'F mul1g pcore_pgroup.
have <-: F = 'F(G).
  apply/eqP; rewrite eqEsubset -{1}(setIidPr sFG) FittingS ?joing_subl //=.
  by rewrite Fitting_max ?Fitting_nil // gFnormal_trans.
apply/trivgP; rewrite /= -(coprime_TIg coGA) subsetI subsetIl andbT.
apply: subset_trans (subset_trans (cent_sub_Fitting solX) sFG).
by rewrite setSI ?joing_subr.
Qed.

(* A "contrapositive" of Proposition 1.4 above.                               *)
Proposition coprime_cent_Fitting gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
  'C_A('F(G)) \subset 'C(G).
Proof.
move=> nGA coGA solG; apply: subset_trans (subsetIr A _); set C := 'C_A(G).
rewrite -quotient_sub1 /= -/C; last first.
  by rewrite subIset // normsI ?normG // norms_cent.
apply: subset_trans (quotient_subcent _ _ _) _; rewrite /= -/C.
have nCG: G \subset 'N(C) by rewrite cents_norm // centsC subsetIr.
rewrite /= -(setIidPr (Fitting_sub _)) -[(G :&: _) / _](morphim_restrm nCG).
rewrite injmF //=; last first.
  by rewrite ker_restrm ker_coset setIA (coprime_TIg coGA) subIset ?subxx.
rewrite morphim_restrm -quotientE setIid.
rewrite coprime_trivg_cent_Fitting ?quotient_norms ?coprime_morph //=.
  exact: morphim_sol.
rewrite -strongest_coprime_quotient_cent ?trivg_quotient ?solG ?orbT //.
  by rewrite -setIA subsetIl.
by rewrite coprime_sym -setIA (coprimegS (subsetIl _ _)).
Qed.

(* B & G Proposition 1.5 is covered by several lemmas in hall.v :             *)
(*  1.5a -> coprime_Hall_exists (internal action)                             *)
(*          ext_coprime_Hall_exists (general group action)                    *)
(*  1.5b -> coprime_Hall_subset (internal action)                             *)
(*          ext_coprime_Hall_subset (general group action)                    *)
(*  1.5c -> coprime_Hall_trans (internal action)                              *)
(*          ext_coprime_Hall_trans (general group action)                     *)
(*  1.5d -> coprime_quotient_cent (internal action)                           *)
(*          ext_coprime_quotient_cent (general group action)                  *)
(*          several stronger variants are proved for internal action          *)
(*  1.5e -> coprime_comm_pcore (internal action only)                         *)

(* A stronger variant of B & G, Proposition 1.6(a). *)
Proposition coprimeR_cent_prod gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|[~: G, A]| #|A| -> solvable [~: G, A] ->
  [~: G, A] * 'C_G(A) = G.
Proof.
move=> nGA coRA solR; apply/eqP; rewrite eqEsubset mulG_subG commg_subl nGA.
rewrite subsetIl -quotientSK ?commg_norml //=.
rewrite coprime_norm_quotient_cent ?commg_normr //=.
by rewrite subsetI subxx quotient_cents2r.
Qed.

(* This is B & G, Proposition 1.6(a). *)
Proposition coprime_cent_prod gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
  [~: G, A] * 'C_G(A) = G.
Proof.
move=> nGA; have sRG: [~: G, A] \subset G by rewrite commg_subl.
rewrite -(Lagrange sRG) coprime_mull => /andP[coRA _] /(solvableS sRG).
exact: coprimeR_cent_prod.
Qed.

(* This is B & G, Proposition 1.6(b). *)
Proposition coprime_commGid gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
  [~: G, A, A] = [~: G, A].
Proof.
move=> nGA coGA solG; apply/eqP; rewrite eqEsubset commSg ?commg_subl //.
have nAC: 'C_G(A) \subset 'N(A) by rewrite subIset ?cent_sub ?orbT.
rewrite -{1}(coprime_cent_prod nGA) // commMG //=; first 1 last.
  by rewrite !normsR // subIset ?normG.
by rewrite (commG1P (subsetIr _ _)) mulg1.
Qed.

(* This is B & G, Proposition 1.6(c). *)
Proposition coprime_commGG1P gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|G| #|A| -> solvable G ->
  [~: G, A, A] = 1 -> A \subset 'C(G).
Proof.
by move=> nGA coGA solG; rewrite centsC coprime_commGid // => /commG1P.
Qed.

(* This is B & G, Proposition 1.6(d), TI-part, from finmod.v *)
Definition coprime_abel_cent_TI := coprime_abel_cent_TI.

(* This is B & G, Proposition 1.6(d) (direct product) *)
Proposition coprime_abelian_cent_dprod gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|G| #|A| -> abelian G ->
  [~: G, A] \x 'C_G(A) = G.
Proof.
move=> nGA coGA abelG; rewrite dprodE ?coprime_cent_prod ?abelian_sol //.
  by rewrite subIset 1?(subset_trans abelG) // centS // commg_subl.
by apply/trivgP; rewrite /= setICA coprime_abel_cent_TI ?subsetIr.
Qed.

(* This is B & G, Proposition 1.6(e), which generalises Aschbacher (24.3). *)
Proposition coprime_abelian_faithful_Ohm1 gT (A G : {group gT}) :
    A \subset 'N(G) -> coprime #|G| #|A| -> abelian G ->
  A \subset 'C('Ohm_1(G)) -> A \subset 'C(G).
Proof.
move=> nGA coGA cGG; rewrite !(centsC A) => cAG1.
have /dprodP[_ defG _ tiRC] := coprime_abelian_cent_dprod nGA coGA cGG.
have sRG: [~: G, A] \subset G by rewrite commg_subl.
rewrite -{}defG -(setIidPl sRG) TI_Ohm1 ?mul1g ?subsetIr //.
by apply/trivgP; rewrite -{}tiRC setIS // subsetI Ohm_sub.
Qed.

(* B & G, Lemma 1.7 is covered by several lemmas in maximal.v :               *)
(*   1.7a -> Phi_nongen                                                       *)
(*   1.7b -> Phi_quotient_abelem                                              *)
(*   1.7c -> trivg_Phi                                                        *)
(*   1.7d -> Phi_joing                                                        *)

(* This is B & G, Proposition 1.8, or Aschbacher 24.1. Note that the coprime  *)
(* assumption is slightly weaker than requiring that A be a p'-group.         *)
Proposition coprime_cent_Phi gT p (A G : {group gT}) :
    p.-group G -> coprime #|G| #|A| -> [~: G, A] \subset 'Phi(G) ->
  A \subset 'C(G).
Proof.
move=> pG coGA sRphi; rewrite centsC; apply/setIidPl.
rewrite -['C_G(A)]genGid; apply/Phi_nongen/eqP.
rewrite eqEsubset join_subG Phi_sub subsetIl -genM_join sub_gen //=.
rewrite -{1}(coprime_cent_prod _ coGA) ?(pgroup_sol pG) ?mulSg //.
by rewrite -commg_subl (subset_trans sRphi) ?Phi_sub.
Qed.

(* This is B & G, Proposition 1.9, base (and most common) case, for internal  *)
(* coprime action.                                                            *)
Proposition stable_factor_cent gT (A G H : {group gT}) :
    A \subset 'C(H) -> stable_factor A H G ->
    coprime #|G| #|A| -> solvable G ->
  A \subset 'C(G).
Proof.
move=> cHA /and3P[sRH sHG nHG] coGA solG.
suffices: G \subset 'C_G(A) by rewrite subsetI subxx centsC.
rewrite -(quotientSGK nHG) ?subsetI ?sHG 1?centsC //.
by rewrite coprime_quotient_cent ?cents_norm ?subsetI ?subxx ?quotient_cents2r.
Qed.

(* This is B & G, Proposition 1.9 (for internal coprime action) *)
Proposition stable_series_cent gT (A G : {group gT}) s :
   last 1%G s :=: G -> (A.-stable).-series 1%G s ->
   coprime #|G| #|A| -> solvable G ->
  A \subset 'C(G).
Proof.
move=> <-{G}; elim/last_ind: s => /= [|s G IHs]; first by rewrite cents1.
rewrite last_rcons rcons_path /= => /andP[/IHs{IHs}].
move: {s}(last _ _) => H IH_H nHGA coGA solG; have [_ sHG _] := and3P nHGA.
by rewrite (stable_factor_cent _ nHGA) ?IH_H ?(solvableS sHG) ?(coprimeSg sHG).
Qed.

(* This is B & G, Proposition 1.10. *)
Proposition coprime_nil_faithful_cent_stab gT (A G : {group gT}) :
     A \subset 'N(G) -> coprime #|G| #|A| -> nilpotent G ->
  let C := 'C_G(A) in 'C_G(C) \subset C -> A \subset 'C(G).
Proof.
move=> nGA coGA nilG C; rewrite subsetI subsetIl centsC /= -/C => cCA.
pose N := 'N_G(C); have sNG: N \subset G by rewrite subsetIl.
have sCG: C \subset G by rewrite subsetIl.
suffices cNA : A \subset 'C(N).
  rewrite centsC (sameP setIidPl eqP) -(nilpotent_sub_norm nilG sCG) //= -/C.
  by rewrite subsetI subsetIl centsC.
have{nilG} solN: solvable N by rewrite(solvableS sNG) ?nilpotent_sol.
rewrite (stable_factor_cent cCA) ?(coprimeSg sNG) /stable_factor //= -/N -/C.
rewrite subcent_normal subsetI (subset_trans (commSg A sNG)) ?commg_subl //=.
rewrite comm_norm_cent_cent 1?centsC ?subsetIr // normsI // !norms_norm //.
by rewrite cents_norm 1?centsC ?subsetIr.
Qed.

(* B & G, Theorem 1.11, via Aschbacher 24.7 rather than Gorenstein 5.3.10. *)
Theorem coprime_odd_faithful_Ohm1 gT p (A G : {group gT}) :
    p.-group G -> A \subset 'N(G) -> coprime #|G| #|A| -> odd #|G| ->
  A \subset 'C('Ohm_1(G)) -> A \subset 'C(G).
Proof.
move=> pG nGA coGA oddG; rewrite !(centsC A) => cAG1.
have [-> | ntG] := eqsVneq G 1; first exact: sub1G.
have{oddG ntG} [p_pr oddp]: prime p /\ odd p.
  have [p_pr p_dv_G _] := pgroup_pdiv pG ntG.
  by rewrite !odd_2'nat in oddG *; rewrite pnatE ?(pgroupP oddG).
without loss defR: G pG nGA coGA cAG1 / [~: G, A] = G.
  move=> IH; have solG := pgroup_sol pG.
  rewrite -(coprime_cent_prod nGA) ?mul_subG ?subsetIr //=.
  have sRG: [~: G, A] \subset G by rewrite commg_subl.
  rewrite IH ?coprime_commGid ?(pgroupS sRG) ?commg_normr ?(coprimeSg sRG) //.
  by apply: subset_trans cAG1; apply: OhmS.
have [|[defPhi defG'] defC] := abelian_charsimple_special pG coGA defR.
  apply/bigcupsP=> H /andP[chH abH]; have sHG := char_sub chH.
  have nHA := char_norm_trans chH nGA.
  rewrite centsC coprime_abelian_faithful_Ohm1 ?(coprimeSg sHG) //.
  by rewrite centsC (subset_trans (OhmS 1 sHG)).
have abelZ: p.-abelem 'Z(G) by apply: center_special_abelem.
have cAZ: {in 'Z(G), centralised A} by apply/centsP; rewrite -defC subsetIr.
have cGZ: {in 'Z(G), centralised G} by apply/centsP; rewrite subsetIr.
have defG1: 'Ohm_1(G) = 'Z(G).
  apply/eqP; rewrite eqEsubset -{1}defC subsetI Ohm_sub cAG1 /=.
  by rewrite -(Ohm1_id abelZ) OhmS ?center_sub.
rewrite (subset_trans _ (subsetIr G _)) // defC -defG1 -{1}defR gen_subG /=.
apply/subsetP=> _ /imset2P[x a Gx Aa ->]; rewrite commgEl.
set u := x^-1; set v := x ^ a; pose w := [~ v, u].
have [Gu Gv]: u \in G /\ v \in G by rewrite groupV memJ_norm ?(subsetP nGA).
have Zw: w \in 'Z(G) by rewrite -defG' mem_commg.
rewrite (OhmE 1 pG) mem_gen // !inE expn1 groupM //=.
rewrite expMg_Rmul /commute ?(cGZ w) // bin2odd // expgM.
case/(abelemP p_pr): abelZ => _ /(_ w)-> //.
rewrite expg1n mulg1 expgVn -conjXg (sameP commgP eqP) cAZ // -defPhi.
by rewrite (Phi_joing pG) joingC mem_gen // inE (Mho_p_elt 1) ?(mem_p_elt pG).
Qed.

(* This is B & G, Corollary 1.12. *)
Corollary coprime_odd_faithful_cent_abelem gT p (A G E : {group gT}) :
    E \in 'E_p(G) -> p.-group G ->
    A \subset 'N(G) -> coprime #|G| #|A| -> odd #|G| ->
  A \subset 'C('Ldiv_p('C_G(E))) -> A \subset 'C(G).
Proof.
case/pElemP=> sEG abelE pG nGA coGA oddG cCEA.
have [-> | ntG] := eqsVneq G 1; first by rewrite cents1.
have [p_pr _ _] := pgroup_pdiv pG ntG.
have{cCEA} cCEA: A \subset 'C('Ohm_1('C_G(E))).
  by rewrite (OhmE 1 (pgroupS _ pG)) ?subsetIl ?cent_gen.
apply: coprime_nil_faithful_cent_stab (pgroup_nil pG) _ => //.
rewrite subsetI subsetIl centsC /=; set CC := 'C_G(_).
have sCCG: CC \subset G := subsetIl _ _; have pCC := pgroupS sCCG pG.
rewrite (coprime_odd_faithful_Ohm1 pCC) ?(coprimeSg sCCG) ?(oddSg sCCG) //.
  by rewrite !(normsI, norms_cent, normG).
rewrite (subset_trans cCEA) // centS // OhmS // setIS // centS //.
rewrite subsetI sEG /= centsC (subset_trans cCEA) // centS //.
have cEE: abelian E := abelem_abelian abelE.
by rewrite -{1}(Ohm1_id abelE) OhmS // subsetI sEG.
Qed.

(* This is B & G, Theorem 1.13.                                               *)
Theorem critical_odd  gT p (G : {group gT}) : 
    p.-group G -> odd #|G| -> G :!=: 1 ->
  {H : {group gT} |
     [/\ H \char G, [~: H, G] \subset 'Z(H), nil_class H <= 2, exponent H = p
       & p.-group 'C(H | [Aut G])]}.
Proof.
move=> pG oddG ntG; have [H krH]:= Thompson_critical pG.
have [chH sPhiZ sGH_Z scH] := krH; have clH := critical_class2 krH.
have sHG := char_sub chH; set D := 'Ohm_1(H)%G; exists D.
have chD: D \char G := char_trans (Ohm_char 1 H) chH.
have sDH: D \subset H := Ohm_sub 1 H.
have sDG_Z: [~: D, G] \subset 'Z(D).
  rewrite subsetI commg_subl char_norm // commGC.
  apply: subset_trans (subset_trans sGH_Z _); first by rewrite commgS.
  by rewrite subIset // orbC centS.
rewrite nil_class2 !(subset_trans (commgS D _) sDG_Z) ?(char_sub chD) {sDH}//.
have [p_pr p_dv_G _] := pgroup_pdiv pG ntG; have odd_p := dvdn_odd p_dv_G oddG.
split=> {chD sDG_Z}//.
  apply/prime_nt_dvdP=> //; last by rewrite exponent_Ohm1_class2 ?(pgroupS sHG).
  rewrite -dvdn1 -trivg_exponent /= Ohm1_eq1; apply: contraNneq ntG => H1.
  by rewrite -(setIidPl (cents1 G)) -{1}H1 scH H1 center1.
apply/pgroupP=> q q_pr /Cauchy[] //= f.
rewrite astab_ract => /setIdP[Af cDf] ofq; apply: wlog_neg => p'q.
suffices: f \in 'C(H | [Aut G]).
  move/(mem_p_elt (critical_p_stab_Aut krH pG))/pnatP=> -> //.
  by rewrite ofq.
rewrite astab_ract inE Af; apply/astabP=> x Hx; rewrite /= /aperm /=.
rewrite nil_class2 in clH; have pH := pgroupS sHG pG.
have /p_natP[i ox]: p.-elt x by apply: mem_p_elt Hx.
have{ox}: x ^+ (p ^ i) = 1 by rewrite -ox expg_order.
elim: i x Hx => [|[|i] IHi] x Hx xp1.
- by rewrite [x]xp1 -(autmE Af) morph1.
- by apply: (astabP cDf); rewrite (OhmE 1 pH) mem_gen // !inE Hx xp1 eqxx.
have expH': {in H &, forall y z, [~ y, z] ^+ p = 1}.
  move=> y z Hy Hz; apply/eqP.
  have /setIP[_ cHyz]: [~ y, z] \in 'Z(H) by rewrite (subsetP clH) // mem_commg.
  rewrite -commXg; last exact/commute_sym/(centP cHyz).
  suffices /setIP[_ cHyp]: y ^+ p \in 'Z(H) by apply/commgP/(centP cHyp).
  rewrite (subsetP sPhiZ) // (Phi_joing pH) mem_gen // inE orbC.
  by rewrite (Mho_p_elt 1) ?(mem_p_elt pH).
have Hfx: f x \in H.
  case/charP: chH => _ /(_ _ (injm_autm Af) (im_autm Af)) <-.
  by rewrite -{1}(autmE Af) mem_morphim // (subsetP sHG).
set y := x^-1 * f x; set z := [~ f x, x^-1].
have Hy: y \in H by rewrite groupM ?groupV.
have /centerP[_ Zz]: z \in 'Z(H) by rewrite (subsetP clH) // mem_commg ?groupV.
have fy: f y = y.
  apply: (IHi); first by rewrite groupM ?groupV.
  rewrite expMg_Rmul; try by apply: commute_sym; apply: Zz; rewrite ?groupV.
  rewrite -/z bin2odd ?odd_exp // {3}expnS -mulnA expgM expH' ?groupV //.
  rewrite expg1n mulg1 expgVn -(autmE Af) -morphX ?(subsetP sHG) //= autmE.
  rewrite IHi ?mulVg ?groupX // {2}expnS expgM -(expgM x _ p) -expnSr.
  by rewrite xp1 expg1n.
have /eqP: (f ^+ q) x = x * y ^+ q.
  elim: (q) => [|j IHj]; first by rewrite perm1 mulg1.
  rewrite expgSr permM {}IHj -(autmE Af).
  rewrite morphM ?morphX ?groupX ?(subsetP sHG) //= autmE.
  by rewrite fy expgS mulgA mulKVg.
rewrite -{1}ofq expg_order perm1 eq_mulVg1 mulKg -order_dvdn.
case: (primeP q_pr) => _ dv_q /dv_q; rewrite order_eq1 -eq_mulVg1.
case/pred2P=> // oyq; case/negP: p'q.
by apply: (pgroupP pH); rewrite // -oyq order_dvdG.
Qed.

Section CoprimeQuotientPgroup.

(* This is B & G, Lemma 1.14, which we divide in four lemmas, each one giving *)
(* the (sub)centraliser or (sub)normaliser of a quotient by a coprime p-group *)
(* acting on it. Note that we weaken the assumptions of B & G -- M does not   *)
(* need to be normal in G, T need not be a subgroup of G, p need not be a     *)
(* prime, and M only needs to be coprime with T. Note also that the subcenter *)
(* quotient lemma is special case of a lemma in coprime_act.                  *)

Variables (gT : finGroupType) (p : nat) (T M G : {group gT}).
Hypothesis pT : p.-group T.
Hypotheses (nMT : T \subset 'N(M)) (coMT : coprime #|M| #|T|).

(* This is B & G, Lemma 1.14, for a global normaliser.                        *)
Lemma coprime_norm_quotient_pgroup : 'N(T / M) = 'N(T) / M.
Proof.
have [-> | ntT] := eqsVneq T 1; first by rewrite quotient1 !norm1 quotientT.
have [p_pr _ [m oMpm]] := pgroup_pdiv pT ntT.
apply/eqP; rewrite eqEsubset morphim_norms // andbT; apply/subsetP=> Mx.
case: (cosetP Mx) => x Nx ->{Mx} nTqMx.
have sylT: p.-Sylow(M <*> T) T.
  rewrite /pHall pT -divgS joing_subr //= norm_joinEr ?coprime_cardMg //.
  rewrite mulnK // ?p'natE -?prime_coprime // coprime_sym.
  by rewrite -(@coprime_pexpr m.+1) -?oMpm.
have sylTx: p.-Sylow(M <*> T) (T :^ x).
  have nMTx: x \in 'N(M <*> T).
    rewrite norm_joinEr // inE -quotientSK ?conj_subG ?mul_subG ?normG //.
    by rewrite quotientJ // quotientMidl (normP nTqMx).
  by rewrite pHallE /= -{1}(normP nMTx) conjSg cardJg -pHallE.
have{sylT sylTx} [ay] := Sylow_trans sylT sylTx.
rewrite /= joingC norm_joinEl //; case/imset2P=> a y Ta.
rewrite -groupV => My ->{ay} defTx; rewrite -(coset_kerr x My).
rewrite mem_morphim //; first by rewrite groupM // (subsetP (normG M)).
by rewrite inE !(conjsgM, defTx) conjsgK conjGid.
Qed.

(* This is B & G, Lemma 1.14, for a global centraliser.                       *)
Lemma coprime_cent_quotient_pgroup : 'C(T / M) = 'C(T) / M.
Proof.
symmetry; rewrite -quotientInorm -quotientMidl -['C(T / M)]cosetpreK.
congr (_ / M); set Cq := _ @*^-1 _; set C := 'N_('C(T))(M).
suffices <-: 'N_Cq(T) = C.
  rewrite setIC group_modl ?sub_cosetpre //= -/Cq; apply/setIidPr.
  rewrite -quotientSK ?subsetIl // cosetpreK.
  by rewrite -coprime_norm_quotient_pgroup cent_sub.
apply/eqP; rewrite eqEsubset subsetI -sub_quotient_pre ?subsetIr //.
rewrite quotientInorm quotient_cents //= andbC subIset ?cent_sub //=.
have nMC': 'N_Cq(T) \subset 'N(M) by rewrite subIset ?subsetIl.
rewrite subsetI nMC' andbT (sameP commG1P trivgP) /=.
rewrite -(coprime_TIg coMT) subsetI commg_subr subsetIr andbT.
by rewrite -quotient_cents2 ?sub_quotient_pre ?subsetIl.
Qed.

Hypothesis sMG : M \subset G.

(* This is B & G, Lemma 1.14, for a local normaliser.                        *)
Lemma coprime_subnorm_quotient_pgroup : 'N_(G / M)(T / M) = 'N_G(T) / M.
Proof. by rewrite quotientGI -?coprime_norm_quotient_pgroup. Qed.

(* This is B & G, Lemma 1.14, for a local centraliser.                       *)
Lemma coprime_subcent_quotient_pgroup : 'C_(G / M)(T / M) = 'C_G(T) / M.
Proof. by rewrite quotientGI -?coprime_cent_quotient_pgroup. Qed.

End CoprimeQuotientPgroup.

Section Constrained.

Variables (gT : finGroupType) (p : nat) (G : {group gT}).

(* This is B & G, Proposition 1.15a (Lemma 1.2.3 of P. Hall & G. Higman). *)
Proposition solvable_p_constrained : solvable G -> p.-constrained G.
Proof.
move=> solG P sylP; have [sPO pP _] := and3P sylP; pose K := 'O_p^'(G).
have nKG: G \subset 'N(K) by rewrite normal_norm ?pcore_normal.
have nKC: 'C_G(P) \subset 'N(K) by rewrite subIset ?nKG.
rewrite -(quotientSGK nKC) //; last first.
  by rewrite /= -pseries1 (pseries_sub_catl [::_]).
apply: subset_trans (quotient_subcent _ _ _) _ ;rewrite /= -/K.
suffices ->: P / K = 'O_p(G / K).
  rewrite quotient_pseries2 -Fitting_eq_pcore ?trivg_pcore_quotient // -/K.
  by rewrite cent_sub_Fitting ?morphim_sol.
apply/eqP; rewrite eqEcard -(part_pnat_id (pcore_pgroup _ _)).
have sylPK: p.-Sylow('O_p(G / K)) (P / K).
  rewrite -quotient_pseries2 morphim_pHall //.
  exact: subset_trans (subset_trans sPO (pseries_sub _ _)) nKG.
by rewrite -(card_Hall sylPK) leqnn -quotient_pseries2 quotientS.
Qed.

(* This is Gorenstein, Proposition 8.1.3. *)
Proposition p_stable_abelian_constrained :
  p.-constrained G -> p.-stable G -> p.-abelian_constrained G.
Proof.
move=> constrG stabG P A sylP cAA /andP[sAP nAP].
have [sPG pP _] := and3P sylP; have sAG := subset_trans sAP sPG.
set K2 := 'O_{p^', p}(G); pose K1 := 'O_p^'(G); pose Q := P :&: K2.
have sQG: Q \subset G by rewrite subIset ?sPG.
have nK1G: G \subset 'N(K1) by rewrite normal_norm ?pcore_normal.
have nsK2G: K2 <| G := pseries_normal _ _; have [sK2G nK2G] := andP nsK2G.
have sylQ: p.-Sylow(K2) Q by rewrite /Q setIC (Sylow_setI_normal nsK2G).
have defK2: K1 * Q = K2.
  have sK12: K1 \subset K2 by rewrite /K1 -pseries1 (pseries_sub_catl [::_]).
  apply/eqP; rewrite eqEsubset mulG_subG /= sK12 subsetIr /=.
  rewrite -quotientSK ?(subset_trans sK2G) //= quotientIG //= -/K1 -/K2.
  rewrite subsetI subxx andbT quotient_pseries2.
  by rewrite pcore_sub_Hall // morphim_pHall // ?(subset_trans sPG).
have{cAA} rQAA_1: [~: Q, A, A] = 1.
  by apply/commG1P; apply: subset_trans cAA; rewrite commg_subr subIset // nAP.
have nK2A := subset_trans sAG nK2G.
have sAN: A \subset 'N_G(Q) by rewrite subsetI sAG normsI // normsG.
have{stabG rQAA_1 defK2 sQG} stabA: A / 'C_G(Q) \subset 'O_p('N_G(Q) / 'C_G(Q)).
  apply: stabG; rewrite //= /psubgroup -/Q ?sAN ?(pgroupS _ pP) ?subsetIl //.
  by rewrite defK2 pseries_normal.
rewrite -quotient_sub1 //= -/K2 -(setIidPr sAN).
have nK2N: 'N_G(Q) \subset 'N(K2) by rewrite subIset ?nK2G.
rewrite -[_ / _](morphim_restrm nK2N); set qK2 := restrm _ _.
have{constrG} fqKp: 'ker (coset 'C_G(Q)) \subset 'ker qK2.
  by rewrite ker_restrm !ker_coset subsetI subcent_sub constrG.
rewrite -(morphim_factm fqKp (subcent_norm _ _)) -(quotientE A _).
apply: subset_trans {stabA}(morphimS _ stabA) _.
apply: subset_trans (morphim_pcore _ _ _) _.
rewrite morphim_factm morphim_restrm setIid -quotientE.
rewrite /= -quotientMidl /= -/K2 (Frattini_arg _ sylQ) ?pseries_normal //.
by rewrite -quotient_pseries //= (pseries_rcons_id [::_]) trivg_quotient.
Qed.

End Constrained.

(* This is B & G, Proposition 1.15b (due to D. Goldschmith). *)
Proposition p'core_cent_pgroup gT p (G R : {group gT}) :
  p.-subgroup(G) R -> solvable G -> 'O_p^'('C_G(R)) \subset 'O_p^'(G).
Proof.
case/andP=> sRG pR solG.
without loss p'G1: gT G R sRG pR solG / 'O_p^'(G) = 1.
  have nOG_CR: 'C_G(R) \subset 'N('O_p^'(G)) by rewrite subIset ?gFnorm.
  move=> IH; rewrite -quotient_sub1 ?gFsub_trans //.
  apply: subset_trans (morphimF _ _ nOG_CR) _; rewrite /= -quotientE.
  rewrite -(coprime_subcent_quotient_pgroup pR) ?pcore_sub //; first 1 last.
  - by rewrite (subset_trans sRG) ?gFnorm.
  - by rewrite coprime_sym (pnat_coprime _ (pcore_pgroup _ _)).
  have p'Gq1 : 'O_p^'(G / 'O_p^'(G)) = 1 := trivg_pcore_quotient p^' G.
  by rewrite -p'Gq1 IH ?morphimS ?morphim_pgroup ?morphim_sol.
set M := 'O_p^'('C_G(R)); pose T := 'O_p(G).
have /subsetIP[sMG cMR]: M \subset 'C_G(R) by apply: pcore_sub.
have [p'M pT]: p^'.-group M /\ p.-group T by rewrite !pcore_pgroup.
have nRT: R \subset 'N(T) by rewrite (subset_trans sRG) ?gFnorm.
have pRT: p.-group (R <*> T).
  rewrite -(pquotient_pgroup pT) ?join_subG ?nRT ?normG //=.
  by rewrite norm_joinEl // quotientMidr morphim_pgroup.
have nRT_M: M \subset 'N(R <*> T).
  by rewrite normsY ?(cents_norm cMR) // (subset_trans sMG) ?gFnorm.
have coRT_M: coprime #|R <*> T| #|M| := pnat_coprime pRT p'M.
have cMcR: 'C_(R <*> T)(R) \subset 'C(M).
  apply/commG1P; apply/trivgP; rewrite -(coprime_TIg coRT_M) subsetI commg_subr.
  rewrite (subset_trans (commSg _ (subsetIl _ _))) ?commg_subl //= -/M.
  by apply: subset_trans (gFnorm _ _); rewrite setSI // join_subG sRG pcore_sub.
have cRT_M: M \subset 'C(R <*> T).
  rewrite coprime_nil_faithful_cent_stab ?(pgroup_nil pRT) //= -/M.
  rewrite subsetI subsetIl (subset_trans _ cMcR) // ?setIS ?centS //.
  by rewrite subsetI joing_subl centsC.
have sMT: M \subset T.
  have defT: 'F(G) = T := Fitting_eq_pcore p'G1.
  rewrite -defT (subset_trans _ (cent_sub_Fitting solG)) // defT subsetI sMG.
  by rewrite (subset_trans cRT_M) // centY subsetIr.
by rewrite -(setIidPr sMT) p'G1 coprime_TIg // (pnat_coprime pT).
Qed.

(* This is B & G, Proposition 1.16, second assertion. Contrary to the text,  *)
(* we derive this directly, rather than by induction on the first, because   *)
(* this is actually how the proof is done in Gorenstein. Note that the non   *)
(* cyclic assumption for A is not needed here.                               *)
Proposition coprime_abelian_gen_cent gT (A G : {group gT}) :
   abelian A -> A \subset 'N(G) -> coprime #|G| #|A| ->
  <<\bigcup_(B : {group gT} | cyclic (A / B) && (B <| A)) 'C_G(B)>> = G.
Proof.
move=> abelA nGA coGA; symmetry; move: {2}_.+1 (ltnSn #|G|) => n.
elim: n gT => // n IHn gT in A G abelA nGA coGA *; rewrite ltnS => leGn.
without loss nilG: G nGA coGA leGn / nilpotent G.
  move=> {IHn} IHn; apply/eqP; rewrite eqEsubset gen_subG.
  apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl.
  pose T := [set P : {group gT} | Sylow G P & A \subset 'N(P)].
  rewrite -{1}(@Sylow_transversal_gen _ T G) => [|P | p _]; first 1 last.
  - by rewrite inE -!andbA; case/and4P.
  - have [//|P sylP nPA] := sol_coprime_Sylow_exists p (abelian_sol abelA) nGA.
    by exists P; rewrite ?inE ?(p_Sylow sylP).
  rewrite gen_subG; apply/bigcupsP=> P {T}/setIdP[/SylowP[p _ sylP] nPA].
  have [sPG pP _] := and3P sylP.
  rewrite (IHn P) ?(pgroup_nil pP) ?(coprimeSg sPG) ?genS //.
    by apply/bigcupsP=> B cycBq; rewrite (bigcup_max B) ?setSI.
  by rewrite (leq_trans (subset_leq_card sPG)).
apply/eqP; rewrite eqEsubset gen_subG.
apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl.
have [Z1 | ntZ] := eqsVneq 'Z(G) 1.
  by rewrite (TI_center_nil _ (normal_refl G)) ?Z1 ?(setIidPr _) ?sub1G.
have{ntZ} [M /= minM] := minnormal_exists ntZ (gFnorm_trans _ nGA).
rewrite subsetI centsC => /andP[sMG /cents_norm nMG]. 
have coMA := coprimeSg sMG coGA; have{nilG} solG := nilpotent_sol nilG.
have [nMA ntM abelM] := minnormal_solvable minM sMG solG.
set GC := <<_>>; have sMGC: M \subset GC.
  rewrite sub_gen ?(bigcup_max 'C_A(M)%G) //=; last first.
    by rewrite subsetI sMG centsC subsetIr.
  case/is_abelemP: abelM => p _ abelM; rewrite -(rker_abelem abelM ntM nMA).
  rewrite rker_normal -(setIidPl (quotient_abelian _ _)) ?center_kquo_cyclic //.
  exact/abelem_mx_irrP.
rewrite -(quotientSGK nMG sMGC).
have: A / M \subset 'N(G / M) by rewrite morphim_norms.
move/IHn->; rewrite ?morphim_abelian ?coprime_morph {IHn}//; first 1 last.
  by rewrite (leq_trans _ leGn) ?ltn_quotient.
rewrite gen_subG; apply/bigcupsP=> Bq; rewrite andbC => /andP[].
have: M :&: A = 1 by rewrite coprime_TIg.
move/(quotient_isom nMA); case/isomP=> /=; set qM := restrm _ _ => injqM <-.
move=> nsBqA; have sBqA := normal_sub nsBqA.
rewrite -(morphpreK sBqA) /= -/qM; set B := qM @*^-1 Bq.
move: nsBqA; rewrite -(morphpre_normal sBqA) ?injmK //= -/B => nsBA.
rewrite -(morphim_quotm _ nsBA) /= -/B injm_cyclic ?injm_quotm //= => cycBA.
rewrite morphim_restrm -quotientE morphpreIdom -/B; have sBA := normal_sub nsBA.
rewrite -coprime_quotient_cent ?(coprimegS sBA, subset_trans sBA) //= -/B.
by rewrite quotientS ?sub_gen // (bigcup_max [group of B]) ?cycBA.
Qed.

(* B & G, Proposition 1.16, first assertion. *)
Proposition coprime_abelian_gen_cent1 gT (A G : {group gT}) :
   abelian A -> ~~ cyclic A -> A \subset 'N(G) -> coprime #|G| #|A| ->
  <<\bigcup_(a in A^#) 'C_G[a]>> = G.
Proof.
move=> abelA ncycA nGA coGA.
apply/eqP; rewrite eq_sym eqEsubset /= gen_subG.
apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl.
rewrite -{1}(coprime_abelian_gen_cent abelA nGA) ?genS //.
apply/bigcupsP=> B; have [-> | /trivgPn[a Ba n1a]] := eqsVneq B 1.
  by rewrite injm_cyclic ?coset1_injm ?norms1 ?(negbTE ncycA).
case/and3P=> _ sBA _; rewrite (bigcup_max a) ?inE ?n1a ?(subsetP sBA) //.
by rewrite setIS // -cent_set1 centS // sub1set.
Qed.

Section Focal_Subgroup.

Variables (gT : finGroupType) (G S : {group gT}) (p : nat).
Hypothesis sylS : p.-Sylow(G) S.

Import finalg FiniteModule GRing.Theory.

(* This is B & G, Theorem 1.17 ("Focal Subgroup Theorem", D. G. Higman), also *)
(* Gorenstein Theorem 7.3.4 and Aschbacher (37.4).                            *)
Theorem focal_subgroup_gen :
  S :&: G^`(1) = <<[set [~ x, u] | x in S, u in G & x ^ u \in S]>>.
Proof.
set K := <<_>>; set G' := G^`(1); have [sSG coSiSG] := andP (pHall_Hall sylS).
apply/eqP; rewrite eqEsubset gen_subG andbC; apply/andP; split.
  apply/subsetP=> _ /imset2P[x u Sx /setIdP[Gu Sxu] ->].
  by rewrite inE groupM ?groupV // mem_commg // (subsetP sSG).
apply/subsetP=> g /setIP[Sg G'g]; have Gg := subsetP sSG g Sg.
have nKS: S \subset 'N(K).
  rewrite norms_gen //; apply/subsetP=> y Sy; rewrite inE.
  apply/subsetP=> _ /imsetP[_ /imset2P[x u Sx /setIdP[Gu Sxu] ->] ->].
  have Gy: y \in G := subsetP sSG y Sy.
  by rewrite conjRg mem_imset2 ?groupJ // inE -conjJg /= 2?groupJ.
set alpha := restrm_morphism nKS (coset_morphism K).
have alphim: (alpha @* S) = (S / K) by rewrite morphim_restrm setIid.
have abelSK : abelian (alpha @* S).
  rewrite alphim sub_der1_abelian // genS //.
  apply/subsetP=> _ /imset2P[x y Sx Sy ->].
  by rewrite mem_imset2 // inE (subsetP sSG) ?groupJ.
set ker_trans := 'ker (transfer G abelSK).
have G'ker : G' \subset ker_trans.
  rewrite gen_subG; apply/subsetP=> h; case/imset2P=> h1 h2 Gh1 Gh2 ->{h}.
  by rewrite !inE groupR // morphR //; apply/commgP; apply: addrC.
have transg0: transfer G abelSK g = 0%R.
  by move/kerP: (subsetP G'ker g G'g); apply.
have partX := rcosets_cycle_partition sSG Gg.
have trX := transversalP partX; set X := transversal _ _ in trX.
have /and3P[_ sXG _] := trX.
have gGSeq0: (fmod abelSK (alpha g) *+ #|G : S| = 0)%R.
  rewrite -transg0 (transfer_cycle_expansion sSG abelSK Gg trX).
  rewrite -(sum_index_rcosets_cycle sSG Gg trX) -sumrMnr /restrm.
  apply: eq_bigr=> x Xx; rewrite -[(_ *+ _)%R]morphX ?mem_morphim //=.
  rewrite -morphX //= /restrm; congr fmod.
  apply/rcoset_kercosetP; rewrite /= -/K.
  - by rewrite (subsetP nKS) ?groupX.
  - rewrite (subsetP nKS) // conjgE invgK mulgA -mem_rcoset.
    exact: mulg_exp_card_rcosets.
  rewrite mem_rcoset -{1}[g ^+ _]invgK -conjVg -commgEl mem_gen ?mem_imset2 //.
    by rewrite groupV groupX.
  rewrite inE conjVg !groupV (subsetP sXG) //= conjgE invgK mulgA -mem_rcoset.
  exact: mulg_exp_card_rcosets.
move: (congr_fmod gGSeq0).
rewrite fmval0 morphX ?inE //= fmodK ?mem_morphim // /restrm /=.
move/((congr1 (expgn^~ (expg_invn (S / K) #|G : S|))) _).
rewrite expg1n expgK ?mem_quotient ?coprime_morphl // => Kg1.
by rewrite coset_idr ?(subsetP nKS).
Qed.

(* This is B & G, Theorem 1.18 (due to Burnside). *)
Theorem Burnside_normal_complement :
  'N_G(S) \subset 'C(S) -> 'O_p^'(G) ><| S = G.
Proof.
move=> cSN; set K := 'O_p^'(G); have [sSG pS _] := and3P sylS.
have /andP[sKG nKG]: K <| G by apply: pcore_normal.
have{nKG} nKS := subset_trans sSG nKG.
have p'K: p^'.-group K by apply: pcore_pgroup.
have{pS p'K} tiKS: K :&: S = 1 by rewrite setIC coprime_TIg ?(pnat_coprime pS).
suffices{tiKS nKS} hallK: p^'.-Hall(G) K.
  rewrite sdprodE //= -/K; apply/eqP; rewrite eqEcard ?mul_subG //=.
  by rewrite TI_cardMg //= (card_Hall sylS) (card_Hall hallK) mulnC partnC.
pose G' := G^`(1); have nsG'G : G' <| G by rewrite der_normalS.
suffices{K sKG} p'G': p^'.-group G'.
  have nsG'K: G' <| K by rewrite (normalS _ sKG) ?pcore_max.
  rewrite -(pquotient_pHall p'G') -?pquotient_pcore //= -/G'.
  by rewrite nilpotent_pcore_Hall ?abelian_nil ?der_abelian.
suffices{nsG'G} tiSG': S :&: G' = 1.
  have sylG'S : p.-Sylow(G') (G' :&: S) by rewrite (Sylow_setI_normal _ sylS).
  rewrite /pgroup -[#|_|](partnC p) ?cardG_gt0 // -{sylG'S}(card_Hall sylG'S).
  by rewrite /= setIC tiSG' cards1 mul1n part_pnat.
apply/trivgP; rewrite /= focal_subgroup_gen ?(p_Sylow sylS) // gen_subG.
apply/subsetP=> _ /imset2P[x u Sx /setIdP[Gu Sxu] ->].
have cSS y: y \in S -> S \subset 'C_G[y].
  rewrite subsetI sSG -cent_set1 centsC sub1set; apply: subsetP.
  by apply: subset_trans cSN; rewrite subsetI sSG normG.
have{cSS} [v]: exists2 v, v \in 'C_G[x ^ u | 'J] & S :=: (S :^ u) :^ v.
  have sylSu : p.-Sylow(G) (S :^ u) by rewrite pHallJ.
  have [sSC sCG] := (cSS _ Sxu, subsetIl G 'C[x ^ u]).
  rewrite astab1J; apply: (@Sylow_trans p); apply: pHall_subl sCG _ => //=.
  by rewrite -conjg_set1 normJ -(conjGid Gu) -conjIg conjSg cSS.
rewrite in_set1 -conjsgM => /setIP[Gv /astab1P cx_uv] nSuv.
apply/conjg_fixP; rewrite -cx_uv /= -conjgM; apply: astabP Sx.
by rewrite astabJ (subsetP cSN) // !inE -nSuv groupM /=.
Qed.

(* This is B & G, Corollary 1.19(a). *)
Corollary cyclic_Sylow_tiVsub_der1 :
  cyclic S -> S :&: G^`(1) = 1 \/ S \subset G^`(1).
Proof.
move=> cycS; have [sSG pS _] := and3P sylS.
have nsSN: S <| 'N_G(S) by rewrite normalSG.
have hallSN: Hall 'N_G(S) S.
  by apply: pHall_Hall (pHall_subl _ _ sylS); rewrite ?subsetIl ?normal_sub.
have /splitsP[K /complP[tiSK /= defN]] := SchurZassenhaus_split hallSN nsSN.
have sKN: K \subset 'N_G(S) by rewrite -defN mulG_subr.
have [sKG nSK] := subsetIP sKN.
have coSK: coprime #|S| #|K|.
  by case/andP: hallSN => sSN; rewrite -divgS //= -defN TI_cardMg ?mulKn.
have:= coprime_abelian_cent_dprod nSK coSK (cyclic_abelian cycS).
case/(cyclic_pgroup_dprod_trivg pS cycS) => [[_ cSK]|[_ <-]]; last first.
  by right; rewrite commgSS.
have cSN: 'N_G(S) \subset 'C(S).
  by rewrite -defN mulG_subG -abelianE cyclic_abelian // centsC -cSK subsetIr.
have /sdprodP[_ /= defG _ _] := Burnside_normal_complement cSN.
set Q := 'O_p^'(G) in defG; have nQG: G \subset 'N(Q) := gFnorm _ _.
left; rewrite coprime_TIg ?(pnat_coprime pS) //.
apply: pgroupS (pcore_pgroup _ G); rewrite /= -/Q.
rewrite -quotient_sub1 ?gFsub_trans ?quotientR //= -/Q.
rewrite -defG quotientMidl (sameP trivgP commG1P) -abelianE.
by rewrite morphim_abelian ?cyclic_abelian.
Qed.

End Focal_Subgroup.

(* This is B & G, Corollary 1.19(b). *)
Corollary Zgroup_der1_Hall gT (G : {group gT}) :
  Zgroup G -> Hall G G^`(1).
Proof.
move=> ZgG; set G' := G^`(1).
rewrite /Hall der_sub coprime_sym coprime_pi' ?cardG_gt0 //=.
apply/pgroupP=> p p_pr pG'; have [P sylP] := Sylow_exists p G.
have cycP: cyclic P by have:= forallP ZgG P; rewrite (p_Sylow sylP).
case: (cyclic_Sylow_tiVsub_der1 sylP cycP) => [tiPG' | sPG'].
  have: p.-Sylow(G') (P :&: G').
    by rewrite setIC (Sylow_setI_normal _ sylP) ?gFnormal.
  move/card_Hall/eqP; rewrite /= tiPG' cards1 eq_sym.
  by rewrite partn_eq1 ?cardG_gt0 // p'natE ?pG'.
rewrite inE /= mem_primes p_pr indexg_gt0 -?p'natE // -partn_eq1 //.
have sylPq: p.-Sylow(G / G') (P / G') by rewrite morphim_pHall ?normsG.
rewrite -card_quotient ?gFnorm // -(card_Hall sylPq) -trivg_card1.
by rewrite /= -quotientMidr mulSGid ?trivg_quotient.
Qed.

(* This is Aschbacher (39.2). *)
Lemma cyclic_pdiv_normal_complement gT (S G : {group gT}) :
  (pdiv #|G|).-Sylow(G) S -> cyclic S -> exists H : {group gT}, H ><| S = G.
Proof.
set p := pdiv _ => sylS cycS; have cSS := cyclic_abelian cycS.
exists 'O_p^'(G)%G; apply: Burnside_normal_complement => //.
have [-> | ntS] := eqsVneq S 1; first apply: cents1.
have [sSG pS p'iSG] := and3P sylS; have [pr_p _ _] := pgroup_pdiv pS ntS.
rewrite -['C(S)]mulg1 -ker_conj_aut -morphimSK ?subsetIr // setIC morphimIdom.
set A_G := _ @* _; pose A := Aut S.
have [_ [_ [cAA _ oAp' _]] _] := cyclic_pgroup_Aut_structure pS cycS ntS.
have{cAA cSS p'iSG} /setIidPl <-: A_G \subset 'O_p^'(A).
  rewrite pcore_max -?sub_abelian_normal ?Aut_conj_aut //=.
  apply: pnat_dvd p'iSG; rewrite card_morphim ker_conj_aut /= setIC.
  have sSN: S \subset 'N_G(S) by rewrite subsetI sSG normG.
  by apply: dvdn_trans (indexSg sSN (subsetIl G 'N(S))); apply: indexgS.
rewrite coprime_TIg ?sub1G // coprime_morphl // coprime_sym coprime_pi' //.
apply/pgroupP=> q pr_q q_dv_G; rewrite !inE mem_primes gtnNdvd ?andbF // oAp'.
by rewrite prednK ?prime_gt0 ?pdiv_min_dvd ?prime_gt1.
Qed.

(* This is Aschbacher (39.3). *)
Lemma Zgroup_metacyclic gT (G : {group gT}) : Zgroup G -> metacyclic G.
Proof.
elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G; rewrite ltnS => leGn ZgG.
have{n IHn leGn} solG: solvable G.
  have [-> | ntG] := eqsVneq G 1; first apply: solvable1.
  have [S sylS] := Sylow_exists (pdiv #|G|) G.
  have cycS: cyclic S := forall_inP ZgG S (p_Sylow sylS).
  have [H defG] := cyclic_pdiv_normal_complement sylS cycS.
  have [nsHG _ _ _ _] := sdprod_context defG; rewrite (series_sol nsHG) andbC.
  rewrite -(isog_sol (sdprod_isog defG)) (abelian_sol (cyclic_abelian cycS)).
  rewrite metacyclic_sol ?IHn ?(ZgroupS _ ZgG) ?normal_sub //.
  rewrite (leq_trans _ leGn) // -(sdprod_card defG) ltn_Pmulr // cardG_gt1.
  by rewrite -rank_gt0 (rank_Sylow sylS) p_rank_gt0 pi_pdiv cardG_gt1.
pose K := 'F(G)%G; apply/metacyclicP; exists K.
have nsKG: K <| G := Fitting_normal G; have [sKG nKG] := andP nsKG.
have cycK: cyclic K by rewrite nil_Zgroup_cyclic ?Fitting_nil ?(ZgroupS sKG).
have cKK: abelian K := cyclic_abelian cycK.
have{solG cKK} defK: 'C_G(K) = K.
  by apply/setP/subset_eqP; rewrite cent_sub_Fitting // subsetI sKG.
rewrite cycK nil_Zgroup_cyclic ?morphim_Zgroup ?abelian_nil //.
rewrite -defK -ker_conj_aut (isog_abelian (first_isog_loc _ _)) //.
exact: abelianS (Aut_conj_aut K G) (Aut_cyclic_abelian cycK).
Qed.

(* This is B & G, Theorem 1.20 (Maschke's Theorem) for internal action on     *)
(* elementary abelian subgroups; a more general case, for linear              *)
(* represenations on matrices, can be found in mxrepresentation.v.            *)
Theorem Maschke_abelem gT p (G V U : {group gT}) :
  p.-abelem V -> p^'.-group G -> U \subset V ->
    G \subset 'N(V) -> G \subset 'N(U) ->
  exists2 W : {group gT}, U \x W = V & G \subset 'N(W).
Proof.
move=> pV p'G sUV nVG nUG.
have splitU: [splits V, over U] := abelem_splits pV sUV.
case/and3P: pV => pV abV; have cUV := subset_trans sUV abV.
have sVVG := joing_subl V G.
have{nUG} nUVG: U <| V <*> G.
  by rewrite /(U <| _) join_subG (subset_trans sUV) // cents_norm // centsC.
rewrite -{nUVG}(Gaschutz_split nUVG) ?(abelianS sUV) // in splitU; last first.
  rewrite -divgS ?joing_subl //= norm_joinEr //.
  have coVG: coprime #|V| #|G| := pnat_coprime pV p'G.
  by rewrite coprime_cardMg // mulnC mulnK // (coprimeSg sUV).
case/splitsP: splitU => WG /complP[tiUWG /= defVG].
exists (WG :&: V)%G.
  rewrite dprodE; last by rewrite setIA tiUWG (setIidPl _) ?sub1G.
    by rewrite group_modl // defVG (setIidPr _).
  by rewrite subIset // orbC centsC cUV.
rewrite (subset_trans (joing_subr V _)) // -defVG mul_subG //.
   by rewrite cents_norm ?(subset_trans cUV) ?centS ?subsetIr.
rewrite normsI ?normG // (subset_trans (mulG_subr U _)) //.
by rewrite defVG join_subG normG.
Qed.

Section Plength1.

Variables (gT : finGroupType) (p : nat).
Implicit Types G H : {group gT}.

(* Some basic properties of p.-length_1 that are direct consequences of their *)
(* definition using p-series.                                                 *)

Lemma plength1_1 : p.-length_1 (1 : {set gT}).
Proof. by rewrite -[_ 1]subG1 pseries_sub. Qed.

Lemma plength1_p'group G : p^'.-group G -> p.-length_1 G.
Proof.
move=> p'G; rewrite [p.-length_1 G]eqEsubset pseries_sub /=.
by rewrite -{1}(pcore_pgroup_id p'G) -pseries1 pseries_sub_catl.
Qed.

Lemma plength1_nonprime G : ~~ prime p -> p.-length_1 G.
Proof.
move=> not_p_pr; rewrite plength1_p'group // p'groupEpi mem_primes.
by rewrite (negPf not_p_pr).
Qed.

Lemma plength1_pcore_quo_Sylow G (Gb := G / 'O_p^'(G)) :
  p.-length_1 G = p.-Sylow(Gb) 'O_p(Gb).
Proof.
rewrite /plength_1 eqEsubset pseries_sub /=.
rewrite (pseries_rcons _ [:: _; _]) -sub_quotient_pre ?gFnorm //=.
rewrite /pHall pcore_sub pcore_pgroup /= -card_quotient ?gFnorm //=.
rewrite -quotient_pseries2 /= {}/Gb -(pseries1 _ G).
rewrite (card_isog (third_isog _ _ _)) ?pseries_normal ?pseries_sub_catl //.
apply/idP/idP=> p'Gbb; last by rewrite (pcore_pgroup_id p'Gbb).
exact: pgroupS p'Gbb (pcore_pgroup _ _).
Qed.

Lemma plength1_pcore_Sylow G :
  'O_p^'(G) = 1 -> p.-length_1 G = p.-Sylow(G) 'O_p(G).
Proof.
move=> p'G1; rewrite plength1_pcore_quo_Sylow -quotient_pseries2.
by rewrite p'G1 pseries_pop2 // pquotient_pHall ?normal1 ?pgroup1.
Qed.

(* This is the characterization given in Section 10 of B & G, p. 75, just     *)
(* before Theorem 10.6.                                                       *)
Lemma plength1_pseries2_quo G : p.-length_1 G = p^'.-group (G / 'O_{p^', p}(G)).
Proof.
rewrite /plength_1 eqEsubset pseries_sub lastI pseries_rcons /=.
rewrite -sub_quotient_pre ?gFnorm //.
by apply/idP/idP=> pl1G; rewrite ?pcore_pgroup_id ?(pgroupS pl1G) ?pcore_pgroup.
Qed.

(* This is B & G, Lemma 1.21(a). *)
Lemma plength1S G H : H \subset G -> p.-length_1 G -> p.-length_1 H.
Proof.
rewrite /plength_1 => sHG pG1; rewrite eqEsubset pseries_sub.
by apply: subset_trans (pseriesS _ sHG); rewrite (eqP pG1) (setIidPr _).
Qed.

Lemma plength1_quo G H : p.-length_1 G -> p.-length_1 (G / H).
Proof.
rewrite /plength_1 => pG1; rewrite eqEsubset pseries_sub.
by rewrite -{1}(eqP pG1) morphim_pseries.
Qed.

(* This is B & G, Lemma 1.21(b). *)
Lemma p'quo_plength1 G H :
  H <| G -> p^'.-group H -> p.-length_1 (G / H) = p.-length_1 G.
Proof.
rewrite /plength_1 => nHG p'H; apply/idP/idP; last exact: plength1_quo.
move=> pGH1; rewrite eqEsubset pseries_sub.
have nOG: 'O_{p^'}(G) <| G by apply: pseries_normal.
rewrite -(quotientSGK (normal_norm nOG)) ?(pseries_sub_catl [:: _]) //.
have [|f f_inj im_f] := third_isom _ nHG nOG.
  by rewrite /= pseries1 pcore_max.
rewrite (quotient_pseries_cat [:: _]) -{}im_f //= -injmF //.
rewrite {f f_inj}morphimS // pseries1 -pquotient_pcore // -pseries1 /=.
by rewrite -quotient_pseries_cat /= (eqP pGH1).
Qed.

(* This is B & G, Lemma 1.21(c). *)
Lemma pquo_plength1 G H :
    H <| G -> p.-group H -> 'O_p^'(G / H) = 1->
  p.-length_1 (G / H) = p.-length_1 G.
Proof.
rewrite /plength_1 => nHG pH trO; apply/idP/idP; last exact: plength1_quo.
rewrite (pseries_pop _ trO) => pGH1; rewrite eqEsubset pseries_sub /=.
rewrite pseries_pop //; last first.
  apply/eqP; rewrite -subG1; have <-: H :&: 'O_p^'(G) = 1.
    by apply: coprime_TIg; apply: pnat_coprime (pcore_pgroup _ _).
  rewrite setIC subsetI subxx -quotient_sub1.
    by rewrite -trO morphim_pcore.
  exact/gFsub_trans/normal_norm.
have nOG: 'O_{p}(G) <| G by apply: pseries_normal.
rewrite -(quotientSGK (normal_norm nOG)) ?(pseries_sub_catl [:: _]) //.
have [|f f_inj im_f] := third_isom _ nHG nOG.
  by rewrite /= pseries1 pcore_max.
rewrite (quotient_pseries [::_]) -{}im_f //= -injmF //.
rewrite {f f_inj}morphimS // pseries1 -pquotient_pcore // -(pseries1 p) /=.
by rewrite -quotient_pseries /= (eqP pGH1).
Qed.

Canonical p_elt_gen_group A : {group gT} :=
  Eval hnf in [group of p_elt_gen p A].

(* Note that p_elt_gen could be a functor. *)
Lemma p_elt_gen_normal G : p_elt_gen p G <| G.
Proof.
apply/normalP; split=> [|x Gx].
  by rewrite gen_subG; apply/subsetP=> x; rewrite inE; case/andP.
rewrite -genJ; congr <<_>>; apply/setP=> y; rewrite mem_conjg !inE.
by rewrite p_eltJ -mem_conjg conjGid.
Qed.

(* This is B & G, Lemma 1.21(d). *)
Lemma p_elt_gen_length1 G :
  p.-length_1 G = p^'.-Hall(p_elt_gen p G) 'O_p^'(p_elt_gen p G).
Proof.
rewrite /pHall pcore_sub pcore_pgroup pnatNK /= /plength_1.
have nUG := p_elt_gen_normal G; have [sUG nnUG]:= andP nUG.
apply/idP/idP=> [p1G | pU].
  apply: (@pnat_dvd _ #|p_elt_gen p G : 'O_p^'(G)|).
    by rewrite -[#|_ : 'O_p^'(G)|]indexgI indexgS ?pcoreS.
  apply: (@pnat_dvd _ #|'O_p(G / 'O_{p^'}(G))|); last exact: pcore_pgroup.
  rewrite -card_quotient; last first.
    by rewrite (subset_trans sUG) // normal_norm ?pcore_normal.
  rewrite -quotient_pseries pseries1 cardSg ?morphimS //=.
  rewrite gen_subG; apply/subsetP=> x; rewrite inE; case/andP=> Gx p_x.
  have nOx: x \in 'N('O_{p^',p}(G)).
    by apply: subsetP Gx; rewrite normal_norm ?pseries_normal.
  rewrite coset_idr //; apply/eqP; rewrite -[coset _ x]expg1 -order_dvdn.
  rewrite [#[_]](@pnat_1 p) //; first exact: morph_p_elt.
  apply: mem_p_elt (pcore_pgroup _ (G / _)) _.
  by rewrite /= -quotient_pseries /= (eqP p1G); apply/morphimP; exists x.
have nOG: 'O_{p^', p}(G) <| G by apply: pseries_normal.
rewrite eqEsubset pseries_sub.
rewrite -(quotientSGK (normal_norm nOG)) ?(pseries_sub_catl [:: _; _]) //=.
rewrite (quotient_pseries [::_;_]) pcore_max //.
rewrite /pgroup card_quotient ?normal_norm //.
apply: pnat_dvd (indexgS G (_ : p_elt_gen p G \subset _)) _; last first.
  case p_pr: (prime p); last by rewrite p'natEpi // mem_primes p_pr.
  rewrite -card_quotient // p'natE //; apply/negP=> /Cauchy[] // Ux.
  case/morphimP=> x Nx Gx -> /= oUx_p; have:= prime_gt1 p_pr.
  rewrite -(part_pnat_id (pnat_id p_pr)) -{1}oUx_p {oUx_p} -order_constt.
  rewrite -morph_constt //= coset_id ?order1 //.
  by rewrite mem_gen // inE groupX // p_elt_constt.
have nOU: p_elt_gen p G \subset 'N('O_{p^'}(G)).
  by rewrite (subset_trans sUG) // normal_norm ?pseries_normal.
rewrite -(quotientSGK nOU) ?(pseries_sub_catl [:: _]) //=.
rewrite (quotient_pseries [::_]) pcore_max ?morphim_normal //.
rewrite /pgroup card_quotient //= pseries1; apply: pnat_dvd pU.
by apply: indexgS; rewrite pcore_max ?pcore_pgroup // gFnormal_trans.
Qed.

End Plength1.

(* This is B & G, Lemma 1.21(e). *)
Lemma quo2_plength1 gT p (G H K : {group gT}) :
  H <| G -> K <| G -> H :&: K = 1 ->
     p.-length_1 (G / H) && p.-length_1 (G / K) = p.-length_1 G.
Proof.
move=> nHG nKG trHK.
have [p_pr | p_nonpr] := boolP (prime p); last by rewrite !plength1_nonprime.
apply/andP/idP=> [[pH1 pK1] | pG1]; last by rewrite !plength1_quo.
pose U := p_elt_gen p G; have nU : U <| G by apply: p_elt_gen_normal.
have exB (N : {group gT}) :
   N <| G -> p.-length_1 (G / N) ->
     exists B : {group gT},
       [/\ U \subset 'N(B),
           forall x, x \in B -> #[x] = p -> x \in N
         & forall Q : {group gT}, p^'.-subgroup(U) Q -> Q \subset B].
- move=> nsNG; have [sNG nNG] := andP nsNG.
  rewrite p_elt_gen_length1 // (_ : p_elt_gen _ _ = U / N); last first.
    rewrite /quotient morphim_gen -?quotientE //; last first.
      by rewrite setIdE subIset ?nNG.
    congr <<_>>; apply/setP=> Nx; rewrite inE setIdE quotientGI // inE.
    apply: andb_id2l => /morphimP[x NNx Gx ->{Nx}] /=.
    apply/idP/idP=> [pNx | /morphimP[y NNy]]; last first.
      by rewrite inE => p_y ->; apply: morph_p_elt.
    rewrite -(constt_p_elt pNx) -morph_constt // mem_morphim ?groupX //.
    by rewrite inE p_elt_constt.
  have nNU: U \subset 'N(N) := subset_trans (normal_sub nU) nNG.
  have nN_UN: U <*> N \subset 'N(N) by rewrite gen_subG subUset normG nNU.
  case/(inv_quotientN _): (pcore_normal p^' [group of U <*> N / N]) => /= [|B].
    by rewrite /normal sub_gen ?subsetUr.
  rewrite /= quotientYidr //= /U => defB sNB; case/andP=> sB nB hallB.
  exists B; split=> [| x Ux p_x | Q /andP[sQU p'Q]].
  - by rewrite (subset_trans (sub_gen _) nB) ?subsetUl.
  - have nNx: x \in 'N(N) by rewrite (subsetP nN_UN) ?(subsetP sB).
    apply: coset_idr => //; rewrite -[coset N x](consttC p).
    rewrite !(constt1P _) ?mulg1 // ?p_eltNK.
      by rewrite morph_p_elt // /p_elt p_x pnat_id.
    have: coset N x \in B / N by apply/morphimP; exists x.
    by apply: mem_p_elt; rewrite /= -defB pcore_pgroup.
  rewrite -(quotientSGK (subset_trans sQU nNU) sNB).
  by rewrite -defB (sub_Hall_pcore hallB) ?quotientS ?quotient_pgroup.
have{pH1} [A [nAU pA p'A]] := exB H nHG pH1.
have{pK1 exB} [B [nBU pB p'B]] := exB K nKG pK1.
rewrite p_elt_gen_length1 //; apply: normal_max_pgroup_Hall (pcore_normal _ _).
apply/maxgroupP; split; first by rewrite /psubgroup pcore_sub pcore_pgroup.
move=> Q p'Q sOQ; apply/eqP; rewrite eqEsubset sOQ andbT.
apply: subset_trans (_ : U :&: (A :&: B) \subset _); last rewrite /U.
  by rewrite !subsetI p'A ?p'B //; case/andP: p'Q => ->.
apply: pcore_max; last by rewrite /normal subsetIl !normsI ?normG.
rewrite /pgroup p'natE //.
apply/negP=> /Cauchy[] // x /setIP[_ /setIP[Ax Bx]] oxp.
suff: x \in 1%G by move/set1P=> x1; rewrite -oxp x1 order1 in p_pr.
by rewrite /= -trHK inE pA ?pB.
Qed.

(* B & G Lemma 1.22 is covered by sylow.normal_pgroup. *)

(* Encapsulation of the use of the order of GL_2(p), via abelem groups. *)
Lemma logn_quotient_cent_abelem gT p (A E : {group gT}) :
    A \subset 'N(E) -> p.-abelem E -> logn p #|E| <= 2 ->
  logn p #|A : 'C_A(E)| <= 1.
Proof.
move=> nEA abelE maxdimE; have [-> | ntE] := eqsVneq E 1.
  by rewrite (setIidPl (cents1 _)) indexgg logn1.
pose rP := abelem_repr abelE ntE nEA.
have [p_pr _ _] := pgroup_pdiv (abelem_pgroup abelE) ntE.
have ->: 'C_A(E) = 'ker (reprGLm rP) by rewrite ker_reprGLm rker_abelem.
rewrite -card_quotient ?ker_norm // (card_isog (first_isog _)).
apply: leq_trans (dvdn_leq_log _ _ (cardSg (subsetT _))) _ => //.
rewrite logn_card_GL_p ?(dim_abelemE abelE) //.
by case: logn maxdimE; do 2?case.
Qed.

End BGsection1.

Section PuigSeriesGroups.

Implicit Type gT : finGroupType.

Canonical Puig_succ_group gT (D E : {set gT}) := [group of 'L_[D](E)].

Fact Puig_at_group_set n gT D : @group_set gT 'L_{n}(D).
Proof. by case: n => [|n]; apply: groupP. Qed.

Canonical Puig_at_group n gT D := Group (@Puig_at_group_set n gT D).
Canonical Puig_inf_group gT (D : {set gT}) := [group of 'L_*(D)].
Canonical Puig_group gT (D : {set gT}) := [group of 'L(D)].

End PuigSeriesGroups.

Notation "''L_[' G ] ( L )" := (Puig_succ_group G L) : Group_scope.
Notation "''L_{' n } ( G )" := (Puig_at_group n G)
  (at level 8, format "''L_{' n } ( G )") : Group_scope.
Notation "''L_*' ( G )" := (Puig_inf_group G) : Group_scope.
Notation "''L' ( G )" := (Puig_group G) : Group_scope.

(* Elementary properties of the Puig series. *)
Section PuigBasics.

Variable gT : finGroupType.
Implicit Types (D E : {set gT}) (G H : {group gT}).

Lemma Puig0 D : 'L_{0}(D) = 1. Proof. by []. Qed.
Lemma PuigS n D : 'L_{n.+1}(D) = 'L_[D]('L_{n}(D)). Proof. by []. Qed.
Lemma Puig_recE n D : Puig_rec n D = 'L_{n}(D). Proof. by []. Qed.
Lemma Puig_def D : 'L(D) = 'L_[D]('L_*(D)). Proof. by []. Qed.

Local Notation "D --> E" := (generated_by (norm_abelian D) E)
  (at level 70, no associativity) : group_scope.

Lemma Puig_gen D E : E --> 'L_[D](E).
Proof. by apply/existsP; exists (subgroups D). Qed.

Lemma Puig_max G D E : D --> E -> E \subset G -> E \subset 'L_[G](D).
Proof.
case/existsP=> gE /eqP <-{E}; rewrite !gen_subG.
move/bigcupsP=> sEG; apply/bigcupsP=> A gEA; have [_ abnA]:= andP gEA.
by rewrite sub_gen // bigcup_sup // inE sEG.
Qed.

Lemma norm_abgenS D1 D2 E : D1 \subset D2 -> D2 --> E -> D1 --> E.
Proof.
move=> sD12 /exists_eqP[gE <-{E}].
apply/exists_eqP; exists [set A in gE | norm_abelian D2 A].
congr <<_>>; apply: eq_bigl => A; rewrite !inE.
apply: andb_idr => /and3P[_ nAD cAA].
by apply/andP; rewrite (subset_trans sD12).
Qed.

Lemma Puig_succ_sub G D : 'L_[G](D) \subset G.
Proof. by rewrite gen_subG; apply/bigcupsP=> A /andP[]; rewrite inE. Qed.

Lemma Puig_at_sub n G : 'L_{n}(G) \subset G.
Proof. by case: n => [|n]; rewrite ?sub1G ?Puig_succ_sub. Qed.

(* This is B & G, Lemma B.1(d), first part. *)
Lemma Puig_inf_sub G : 'L_*(G) \subset G.
Proof. exact: Puig_at_sub. Qed.

Lemma Puig_sub G : 'L(G) \subset G.
Proof. exact: Puig_at_sub. Qed.

(* This is part of B & G, Lemma B.1(b). *)
Lemma Puig1 G : 'L_{1}(G) = G.
Proof.
apply/eqP; rewrite eqEsubset Puig_at_sub; apply/subsetP=> x Gx.
rewrite -cycle_subG sub_gen // -[<[x]>]/(gval _) bigcup_sup //=.
by rewrite inE cycle_subG Gx /= /norm_abelian cycle_abelian sub1G.
Qed.

End PuigBasics.

(* Functoriality of the Puig series. *)

Fact Puig_at_cont n : GFunctor.iso_continuous (Puig_at n).
Proof.
elim: n => [|n IHn] aT rT G f injf; first by rewrite morphim1.
have IHnS := Puig_at_sub n; pose func_n := [igFun by IHnS & !IHn].
rewrite !PuigS sub_morphim_pre ?Puig_succ_sub // gen_subG; apply/bigcupsP=> A.
rewrite inE => /and3P[sAG nAL cAA]; rewrite -sub_morphim_pre ?sub_gen //.
rewrite -[f @* A]/(gval _) bigcup_sup // inE morphimS // /norm_abelian.
rewrite morphim_abelian // -['L_{n}(_)](injmF func_n injf) //=.
by rewrite morphim_norms.
Qed.

Canonical Puig_at_igFun n := [igFun by Puig_at_sub^~ n & !Puig_at_cont n].

Fact Puig_inf_cont : GFunctor.iso_continuous Puig_inf.
Proof.
by move=> aT rT G f injf; rewrite /Puig_inf card_injm // Puig_at_cont.
Qed.

Canonical Puig_inf_igFun := [igFun by Puig_inf_sub & !Puig_inf_cont].

Fact Puig_cont : GFunctor.iso_continuous Puig.
Proof. by move=> aT rT G f injf; rewrite /Puig card_injm // Puig_at_cont. Qed.

Canonical Puig_igFun := [igFun by Puig_sub & !Puig_cont].