path: root/mathcomp/odd_order/BGsection3.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.
From mathcomp
Require Import fintype tuple bigop prime binomial finset ssralg fingroup finalg.
From mathcomp
Require Import morphism perm automorphism quotient action commutator gproduct.
From mathcomp
Require Import zmodp cyclic gfunctor center pgroup gseries nilpotent sylow.
From mathcomp
Require Import finmodule abelian frobenius maximal extremal hall.
From mathcomp
Require Import matrix mxalgebra mxrepresentation mxabelem wielandt_fixpoint.
From mathcomp
Require Import BGsection1 BGsection2.

(******************************************************************************)
(*   This file covers the material in B & G, Section 3.                       *)
(*   Note that in spite of the use of Gorenstein 2.7.6, the material in all   *)
(* of Section 3, and in all likelyhood the whole of B & G, does NOT depend on *)
(* the general proof of existence of Frobenius kernels, because results on    *)
(* Frobenius groups are only used when the semidirect product decomposition   *)
(* is already known, and (see file frobenius.v) in this case the kernel is    *)
(* equal to the normal complement of the Frobenius complement.                *)
(******************************************************************************)

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

Local Open Scope ring_scope.
Import GroupScope GRing.Theory.

Section BGsection3.

Implicit Type F : fieldType.
Implicit Type gT : finGroupType.
Implicit Type p : nat.

(* B & G, Lemma 3.1 is covered by frobenius.Frobenius_semiregularP. *)

(* This is B & G, Lemma 3.2. *)
Section FrobeniusQuotient.

Variables (gT : finGroupType) (G K R : {group gT}).
Implicit Type N : {group gT}.

(* This is a special case of B & G, Lemma 3.2 (b). *)
Lemma Frobenius_proper_quotient N :
    [Frobenius G = K ><| R] -> solvable K -> N <| G -> N \proper K ->
  [Frobenius G / N = (K / N) ><| (R / N)].
Proof.
move=> frobG solK nsNG /andP[sNK ltNK].
have [defG _ ntR _ _] := Frobenius_context frobG.
have [nsKG sRG defKR nKR tiKR] := sdprod_context defG; have [sKG _]:= andP nsKG.
have nsNK := normalS sNK sKG nsNG.
apply/Frobenius_semiregularP=> [|||Nx].
- rewrite sdprodE ?quotient_norms //.
    by rewrite -quotientMl ?defKR ?normal_norm.
  by rewrite -quotientGI // tiKR quotient1.
- by rewrite -subG1 quotient_sub1 ?normal_norm.
- rewrite -subG1 quotient_sub1; last by rewrite (subset_trans sRG) ?normal_norm.
  apply: contra ntR => sRN.
  by rewrite -subG1 -tiKR subsetI (subset_trans sRN) /=.
rewrite !inE andbC => /andP[/morphimP[x nNx Rx ->{Nx}] notNx].
apply/trivgP; rewrite /= -cent_cycle -quotient_cycle //.
rewrite -coprime_quotient_cent ?cycle_subG //; last first.
  by apply: coprimegS (Frobenius_coprime frobG); rewrite cycle_subG.
rewrite cent_cycle (Frobenius_reg_ker frobG) ?quotient1 // !inE Rx andbT.
by apply: contraNneq notNx => ->; rewrite morph1.
Qed.

(* This is B & G, Lemma 3.2 (a). *)
Lemma Frobenius_normal_proper_ker N :
    [Frobenius G = K ><| R] -> solvable K -> N <| G -> ~~ (K \subset N) ->
  N \proper K.
Proof.
move=> frobG solK nsNG ltNK; have [sNG nNG] := andP nsNG; pose H := N :&: K.
have [defG _ ntR _ _] := Frobenius_context frobG.
have [nsKG _ /mulG_sub[sKG _] nKR tiKR] := sdprod_context defG.
have nsHG: H <| G := normalI nsNG nsKG; have [_ nHG] := andP nsHG.
have ltHK: H \proper K by rewrite /proper subsetIr subsetI subxx andbT.
suffices /eqP tiNR: N :&: R == 1.
  rewrite /proper ltNK andbT -(setIidPl sNG).
  rewrite -(cover_partition (Frobenius_partition frobG)) big_distrr /=.
  apply/bigcupsP=> _ /setU1P[->| /imsetP[x Kx ->]]; first exact: subsetIr.
  rewrite conjD1g setIDA subDset -(normsP (subset_trans sKG nNG) x) //.
  by rewrite -conjIg tiNR conjs1g subsetUl.
suffices: (N :&: R) / H \subset [1].
  by rewrite -subG1 quotient_sub1 ?normsGI // -subsetIidr setIACA tiKR setIg1.
have frobGq := Frobenius_proper_quotient frobG solK nsHG ltHK.
have [_ ntKq _ _ _] := Frobenius_context frobGq.
rewrite -(cent_semiregular (Frobenius_reg_compl frobGq) _ ntKq) //.
rewrite subsetI quotientS ?subsetIr // quotient_cents2r //.
by rewrite commg_subI ?setIS // subsetIidl (subset_trans sKG).
Qed.

(* This is B & G, Lemma 3.2 (b). *)
Lemma Frobenius_quotient N :
    [Frobenius G = K ><| R] -> solvable K -> N <| G -> ~~ (K \subset N) ->
  [Frobenius G / N = (K / N) ><| (R / N)].
Proof.
move=> frobG solK nsNG ltKN; apply: Frobenius_proper_quotient => //.
exact: (Frobenius_normal_proper_ker frobG).
Qed.

End FrobeniusQuotient.

(* This is B & G, Lemma 3.3. *)
Lemma Frobenius_rfix_compl F gT (G K R : {group gT}) n
                          (rG : mx_representation F G n) :
    [Frobenius G = K ><| R] -> [char F]^'.-group K ->
  ~~ (K \subset rker rG) -> rfix_mx rG R != 0.
Proof.
rewrite /pgroup charf'_nat => frobG nzK.
have [defG _ _ ltKG ltRG]:= Frobenius_context frobG.
have{ltKG ltRG} [sKG sRG]: K \subset G /\ R \subset G by rewrite !proper_sub.
apply: contraNneq => fixR0; rewrite rfix_mx_rstabC // -(eqmx_scale _ nzK).
pose gsum H := gring_op rG (gset_mx F G H).
have fixsum (H : {group gT}): H \subset G -> (gsum H <= rfix_mx rG H)%MS.
  move/subsetP=> sHG; apply/rfix_mxP=> x Hx; have Gx := sHG x Hx.
  rewrite -gring_opG // -gring_opM ?envelop_mx_id //; congr (gring_op _ _).
  rewrite {2}/gset_mx (reindex_acts 'R _ Hx) ?astabsR //= mulmx_suml.
  by apply:eq_bigr=> y; move/sHG=> Gy; rewrite repr_mxM.
have: gsum G + rG 1 *+ #|K| = gsum K + \sum_(x in K) gsum (R :^ x).
  rewrite -gring_opG // -sumr_const -!linear_sum -!linearD; congr gring_op.
  rewrite {1}/gset_mx (set_partition_big _ (Frobenius_partition frobG)) /=.
  rewrite big_setU1 -?addrA /=; last first.
    by apply: contraL (group1 K) => /imsetP[x _ ->]; rewrite conjD1g !inE eqxx.
  congr (_ + _); rewrite big_imset /= => [|x y Kx Ky /= eqRxy]; last first.
    have [/eqP/sdprodP[_ _ _ tiKR] _ _ _ /eqP snRG] := and5P frobG.
    apply/eqP; rewrite eq_mulgV1 -in_set1 -set1gE -tiKR -snRG setIA.
    by rewrite (setIidPl sKG) !inE conjsgM eqRxy actK groupM /= ?groupV.
  rewrite -big_split; apply: eq_bigr => x Kx /=.
  by rewrite addrC conjD1g -big_setD1 ?group1.
have ->: gsum G = 0.
  apply/eqP; rewrite -submx0 -fixR0; apply: submx_trans (rfix_mxS rG sRG).
  exact: fixsum.
rewrite repr_mx1 -scaler_nat add0r => ->.
rewrite big1 ?addr0 ?fixsum // => x Kx; have Gx := subsetP sKG x Kx.
apply/eqP; rewrite -submx0 (submx_trans (fixsum _ _)) ?conj_subG //.
by rewrite -(mul0mx _ (rG x)) -fixR0 rfix_mx_conjsg.
Qed.

(* This is Aschbacher (40.6)(3), or G. (3.14)(iii). *)
Lemma regular_pq_group_cyclic gT p q (H R : {group gT}) :
    [/\ prime p, prime q & p != q] -> #|R| = (p * q)%N ->
    H :!=: 1 -> R \subset 'N(H) -> semiregular H R ->
  cyclic R.
Proof.
case=> pr_p pr_q q'p oR ntH nHR regHR.
without loss{q'p} ltpq: p q pr_p pr_q oR / p < q.
  by move=> IH; case: ltngtP q'p => // /IH-> //; rewrite mulnC.
have [p_gt0 q_gt0]: 0 < p /\ 0 < q by rewrite !prime_gt0.
have [[P sylP] [Q sylQ]] := (Sylow_exists p R, Sylow_exists q R).
have [sPR sQR] := (pHall_sub sylP, pHall_sub sylQ).
have [oP oQ]: #|P| = p /\ #|Q| = q.
  rewrite (card_Hall sylQ) (card_Hall sylP) oR !p_part !lognM ?logn_prime //.
  by rewrite !eqxx eq_sym gtn_eqF.
have [ntP ntQ]: P :!=: 1 /\ Q :!=: 1 by rewrite -!cardG_gt1 oP oQ !prime_gt1.
have nQR: R \subset 'N(Q).
  rewrite -subsetIidl -indexg_eq1 -(card_Syl_mod R pr_q) (card_Syl sylQ) /=.
  rewrite modn_small // -divgS ?subsetIl ?ltn_divLR // mulnC oR ltn_pmul2r //.
  by rewrite (leq_trans ltpq) // -oQ subset_leq_card // subsetI sQR normG.
have coQP: coprime #|Q| #|P|.
  by rewrite oP oQ prime_coprime ?dvdn_prime2 ?gtn_eqF.
have defR: Q ><| P = R.
  rewrite sdprodE ?coprime_TIg ?(subset_trans sPR) //.
  by apply/eqP; rewrite eqEcard mul_subG //= oR coprime_cardMg // oP oQ mulnC.
have [cycP cycQ]: cyclic P /\ cyclic Q by rewrite !prime_cyclic ?oP ?oQ.
suffices cQP: P \subset 'C(Q) by rewrite (@cyclic_dprod _ Q P) ?dprodEsd.
without loss /is_abelemP[r pr_r abelH]: H ntH nHR regHR / is_abelem H.
  move=> IH; have [r _ rH] := rank_witness H.
  have solR: solvable R.
    apply/metacyclic_sol/metacyclicP; exists Q.
    by rewrite /(Q <| R) sQR -(isog_cyclic (sdprod_isog defR)).
  have coHR: coprime #|H| #|R| := regular_norm_coprime nHR regHR.
  have [H1 sylH1 nH1R] := sol_coprime_Sylow_exists r solR nHR coHR.
  have ntH1: H1 :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylH1) -rH rank_gt0.
  have [H2 minH2 sH21] := minnormal_exists ntH1 nH1R.
  have [sH1H rH1 _] := and3P sylH1; have sH2H := subset_trans sH21 sH1H.
  have [nH2R ntH2 abelH2] := minnormal_solvable minH2 sH21 (pgroup_sol rH1).
  by apply: IH abelH2 => //; apply: semiregularS regHR.
have: rfix_mx (abelem_repr abelH ntH nHR) P == 0.
  rewrite -mxrank_eq0 rfix_abelem // mxrank_eq0 rowg_mx_eq0 /=.
  by rewrite (cent_semiregular regHR) ?morphim1.
apply: contraLR => not_cQP; have{not_cQP} frobR: [Frobenius R = Q ><| P].
  by apply/prime_FrobeniusP; rewrite ?prime_TIg ?oP ?oQ // centsC.
apply: (Frobenius_rfix_compl frobR).
  rewrite (eq_p'group _ (charf_eq (char_Fp pr_r))).
  rewrite (coprime_p'group _ (abelem_pgroup abelH)) //.
  by rewrite coprime_sym (coprimegS sQR) ?regular_norm_coprime.
rewrite rker_abelem subsetI sQR centsC.
by rewrite -subsetIidl (cent_semiregular regHR) ?subG1.
Qed.

(* This is B & G, Theorem 3.4. *)
Theorem odd_prime_sdprod_rfix0 F gT (G K R : {group gT}) n 
                               (rG : mx_representation F G n) :
    K ><| R = G -> solvable G -> odd #|G| -> coprime #|K| #|R| -> prime #|R| ->
    [char F]^'.-group G -> rfix_mx rG R = 0 ->
  [~: R, K] \subset rker rG.
Proof.
move: {2}_.+1 (ltnSn #|G|) => m; elim: m => // m IHm in gT G K R n rG *.
rewrite ltnS; set p := #|R| => leGm defG solG oddG coKR p_pr F'G regR.
have [nsKG sRG defKR nKR tiKR] := sdprod_context defG.
have [sKG nKG] := andP nsKG; have solK := solvableS sKG solG.
have [-> | ntK] := eqsVneq K 1; first by rewrite commG1 sub1G.
have ker_ltK (H : {group gT}):
  H \proper K -> R \subset 'N(H) -> [~: R, H] \subset rker rG.
- move=> ltKH nHR; have sHK := proper_sub ltKH; set G1 := H <*> R.
  have sG1G: G1 \subset G by rewrite join_subG (subset_trans sHK).
  have coHR := coprimeSg sHK coKR.
  have defG1: H ><| R = G1 by rewrite sdprodEY // coprime_TIg.
  apply: subset_trans (subsetIr G1 _); rewrite -(rker_subg _ sG1G).
  apply: IHm; rewrite ?(solvableS sG1G) ?(oddSg sG1G) ?(pgroupS sG1G) //.
  apply: leq_trans leGm; rewrite /= norm_joinEr // -defKR !coprime_cardMg //.
  by rewrite ltn_pmul2r ?proper_card.
without loss [q q_pr qK]: / exists2 q, prime q & q.-group K.
  move=> IH; set q := pdiv #|K|.
  have q_pr: prime q by rewrite pdiv_prime ?cardG_gt1.
  have exHall := coprime_Hall_exists _ nKR coKR solK.
  have [Q sylQ nQR] := exHall q; have [Q' hallQ' nQ'R] := exHall q^'.
  have [sQK qQ _] := and3P sylQ; have [sQ'K q'Q' _] := and3P hallQ'.
  without loss{IH} ltQK: / Q \proper K.
    by rewrite properEneq; case: eqP IH => [<- -> | _ _ ->] //; exists q.
  have ltQ'K: Q' \proper K.
    rewrite properEneq; case: eqP (pgroupP q'Q' q q_pr) => //= ->.
    by rewrite !inE pdiv_dvd eqxx; apply.
  have nkerG := subset_trans _ (rker_norm rG).
  rewrite -quotient_cents2 ?nkerG //.
  have <-: Q * Q' = K.
    apply/eqP; rewrite eqEcard mulG_subG sQK sQ'K.
    rewrite coprime_cardMg ?(pnat_coprime qQ) //=.
    by rewrite (card_Hall sylQ) (card_Hall hallQ') partnC.
  rewrite quotientMl ?nkerG ?(subset_trans sQK) // centM subsetI.
  by rewrite !quotient_cents2r ?ker_ltK.
without loss{m IHm leGm} [ffulG cycZ]: / rker rG = 1 /\ cyclic 'Z(G).
  move=> IH; wlog [I M /= simM sumM _]: / mxsemisimple rG 1%:M.
    exact: (mx_reducible_semisimple (mxmodule1 _) (mx_Maschke _ F'G)).
  pose not_cRK_M i := ~~ ([~: R, K] \subset rstab rG (M i)).
  case: (pickP not_cRK_M) => [i | cRK_M]; last first.
    rewrite rfix_mx_rstabC ?comm_subG // -sumM.
    apply/sumsmx_subP=> i _; move/negbFE: (cRK_M i).
    by rewrite rfix_mx_rstabC ?comm_subG.
  have [modM ntM _] := simM i; pose rM := kquo_repr (submod_repr modM).
  do [rewrite {+}/not_cRK_M -(rker_submod modM) /=; set N := rker _] in rM *.
  have [N1 _ | ntN] := eqVneq N 1.
    apply: IH; split.
      by apply/trivgP; rewrite -N1 /N rker_submod rstabS ?submx1.
    have: mx_irreducible (submod_repr modM) by apply/submod_mx_irr.
    by apply: mx_faithful_irr_center_cyclic; apply/trivgP.
  have tiRN: R :&: N = 1.
    by apply: prime_TIg; rewrite //= rker_submod rfix_mx_rstabC // regR submx0.
  have nsNG: N <| G := rker_normal _; have [sNG nNG] := andP nsNG.
  have nNR := subset_trans sRG nNG.
  have sNK: N \subset K.
    have [pi hallK]: exists pi, pi.-Hall(G) K.
      by apply: HallP; rewrite -(coprime_sdprod_Hall_l defG).
    rewrite (sub_normal_Hall hallK) //=.
    apply: pnat_dvd (pHall_pgroup hallK).
    rewrite -(dvdn_pmul2r (prime_gt0 p_pr)) -!TI_cardMg // 1?setIC // defKR.
    by rewrite -norm_joinEr // cardSg // join_subG sNG.
  have defGq: (K / N) ><| (R / N) = G / N.
    rewrite sdprodE ?quotient_norms -?quotientMr ?defKR //.
    by rewrite -quotientGI // tiKR quotient1.
  case/negP; rewrite -quotient_cents2  ?(subset_trans _ nNG) //= -/N.
  rewrite (sameP commG1P trivgP).
  apply: subset_trans (kquo_mx_faithful (submod_repr modM)).
  rewrite IHm ?quotient_sol ?coprime_morph ?morphim_odd ?quotient_pgroup //.
  - by apply: leq_trans leGm; apply: ltn_quotient.
  - by rewrite card_quotient // -indexgI tiRN indexg1.
  apply/eqP; rewrite -submx0 rfix_quo // rfix_submod //.
  by rewrite regR capmx0 linear0 sub0mx.
without loss perfectK: / [~: K, R] = K.
  move=> IH; have: [~: K, R] \subset K by rewrite commg_subl.
  rewrite subEproper; case/predU1P=> //; move/ker_ltK.
  by rewrite commGC commg_normr coprime_commGid // commGC => ->.
have primeR: {in R^#, forall x, 'C_K[x] = 'C_K(R)}.
  move=> x; case/setD1P=> nt_x Rx; rewrite -cent_cycle ((<[x]> =P R) _) //.
  rewrite eqEsubset cycle_subG Rx; apply: contraR nt_x; move/prime_TIg.
  by rewrite -cycle_eq1 (setIidPr _) ?cycle_subG // => ->.
case cKK: (abelian K).
  rewrite commGC perfectK; move/eqP: regR; apply: contraLR.
  apply: Frobenius_rfix_compl => //; last exact: pgroupS F'G.
  rewrite -{2 4}perfectK coprime_abel_cent_TI // in primeR.
  by apply/Frobenius_semiregularP; rewrite // -cardG_gt1 prime_gt1.
have [spK defZK]: special K /\ 'C_K(R) = 'Z(K).
  apply: (abelian_charsimple_special qK) => //.
  apply/bigcupsP=> H /andP[chHK cHH].
  have:= char_sub chHK; rewrite subEproper.
  case/predU1P=> [eqHK | ltHK]; first by rewrite eqHK cKK in cHH.
  have nHR: R \subset 'N(H) := char_norm_trans chHK nKR.
  by rewrite (sameP commG1P trivgP) /= commGC -ffulG ker_ltK.
have{spK} esK: extraspecial K.
  have abelZK := center_special_abelem qK spK; have [qZK _] := andP abelZK.
  have /(pgroup_pdiv qZK)[_ _ []]: 'Z(K) != 1.
    by case: spK => _ <-; rewrite (sameP eqP commG1P) -abelianE cKK.
  case=> [|e] oK; first by split; rewrite ?oK.
  suffices: cyclic 'Z(K) by rewrite (abelem_cyclic abelZK) oK pfactorK.
  rewrite (cyclicS _ cycZ) // subsetI subIset ?sKG //=.
  by rewrite -defKR centM subsetI -{2}defZK !subsetIr.
have [e e_gt0 oKqe] := card_extraspecial qK esK.
have cycR: cyclic R := prime_cyclic p_pr.
have co_q_p: coprime q p by rewrite oKqe coprime_pexpl in coKR.
move/eqP: regR; case/idPn.
rewrite defZK in primeR.
case: (repr_extraspecial_prime_sdprod_cycle _ _ defG _ oKqe) => // _.
apply=> //; last exact/trivgP.
apply: contraL (oddSg sRG oddG); move/eqP->; have:= oddSg sKG oddG.
by rewrite oKqe addn1 /= !odd_exp /= orbC => ->.
Qed.

(* Internal action version of B & G, Theorem 3.4. *)
Theorem odd_prime_sdprod_abelem_cent1 k gT (G K R V : {group gT}) :
    solvable G -> odd #|G| -> K ><| R = G -> coprime #|K| #|R| -> prime #|R| ->
    k.-abelem V -> G \subset 'N(V) -> k^'.-group G -> 'C_V(R) = 1 ->
  [~: R, K] \subset 'C_K(V).
Proof.
move=> solG oddG defG coKR prR abelV nVG k'G regR.
have [_ sRG _ nKR _] := sdprod_context defG; rewrite subsetI commg_subr nKR.
case: (eqsVneq V 1) => [-> | ntV]; first exact: cents1.
pose rV := abelem_repr abelV ntV nVG.
apply: subset_trans (_ : rker rV \subset _); last first.
  by rewrite rker_abelem subsetIr.
apply: odd_prime_sdprod_rfix0 => //.
  have k_pr: prime k by case/pgroup_pdiv: (abelem_pgroup abelV).
  by rewrite (eq_pgroup G (eq_negn (charf_eq (char_Fp k_pr)))).
by apply/eqP; rewrite -submx0 rfix_abelem //= regR morphim1 rowg_mx1.
Qed.

(* This is B & G, Theorem 3.5. *)
Theorem Frobenius_prime_rfix1 F gT (G K R : {group gT}) n
                              (rG : mx_representation F G n) :
    K ><| R = G -> solvable G -> prime #|R| -> 'C_K(R) = 1 ->
    [char F]^'.-group G -> \rank (rfix_mx rG R) = 1%N ->
  K^`(1) \subset rker rG.
Proof.
move=> defG solG p_pr regR F'G fixRlin.
wlog closF: F rG F'G fixRlin / group_closure_field F gT.
  move=> IH; apply: (@group_closure_field_exists gT F) => [[Fc f closFc]].
  rewrite -(rker_map f) IH //; last by rewrite -map_rfix_mx mxrank_map.
  by rewrite (eq_p'group _ (fmorph_char f)).
move: {2}_.+1 (ltnSn #|K|) => m.
elim: m => // m IHm in gT G K R rG solG p_pr regR F'G closF fixRlin defG *.
rewrite ltnS => leKm.
have [nsKG sRG defKR nKR tiKR] := sdprod_context defG.
have [sKG nKG] := andP nsKG; have solK := solvableS sKG solG.
have cycR := prime_cyclic p_pr.
case: (eqsVneq K 1) => [-> | ntK]; first by rewrite derg1 commG1 sub1G.
have defR x: x \in R^# -> <[x]> = R.  
  case/setD1P; rewrite -cycle_subG -cycle_eq1 => ntX sXR.
  apply/eqP; rewrite eqEsubset sXR; apply: contraR ntX => /(prime_TIg p_pr).
  by rewrite /= (setIidPr sXR) => ->.
have ntR: R :!=: 1 by rewrite -cardG_gt1 prime_gt1.
have frobG: [Frobenius G = K ><| R].
  by apply/Frobenius_semiregularP=> // x Rx; rewrite -cent_cycle defR.
case: (eqVneq (rker rG) 1) => [ffulG | ntC]; last first.
  set C := rker rG in ntC *; have nsCG: C <| G := rker_normal rG.
  have [sCG nCG] := andP nsCG.
  have nCK := subset_trans sKG nCG; have nCR := subset_trans sRG nCG.
  case sKC: (K \subset C); first exact: gFsub_trans.
  have sCK: C \subset K.
    by rewrite proper_sub // (Frobenius_normal_proper_ker frobG) ?sKC.
  have frobGq: [Frobenius G / C = (K / C) ><| (R / C)].
    by apply: Frobenius_quotient; rewrite ?sKC.
  have [defGq _ ntRq _ _] := Frobenius_context frobGq.
  rewrite -quotient_sub1 ?comm_subG ?quotient_der //= -/C.
  apply: subset_trans (kquo_mx_faithful rG).
  apply: IHm defGq _; rewrite 1?(quotient_sol, quotient_pgroup, rfix_quo) //.
  - rewrite card_quotient // -indexgI /= -/C setIC.
    by rewrite -(setIidPl sCK) -setIA tiKR (setIidPr (sub1G _)) indexg1.
  - have: cyclic (R / C) by [rewrite quotient_cyclic]; case/cyclicP=> Cx defRq.
    rewrite /= defRq cent_cycle (Frobenius_reg_ker frobGq) //= !inE defRq.
    by rewrite cycle_id -cycle_eq1 -defRq ntRq.
  - move=> Hq; rewrite -(group_inj (cosetpreK Hq)).
    by apply: quotient_splitting_field; rewrite ?subsetIl.
  by apply: leq_trans leKm; apply: ltn_quotient.
have ltK_abelian (N : {group gT}): R \subset 'N(N) -> N \proper K -> abelian N.
  move=> nNR ltNK; have [sNK _] := andP ltNK; apply/commG1P/trivgP.
  rewrite -(setIidPr (sub1G (N <*> R))) /= -ffulG; set G1 := N <*> R.
  have sG1: G1 \subset G by rewrite join_subG (subset_trans sNK).
  have defG1: N ><| R = G1.
    by rewrite sdprodEY //; apply/trivgP; rewrite -tiKR setSI.
  rewrite -(rker_subg _ sG1).
  apply: IHm defG1 _; rewrite ?(solvableS sG1) ?(pgroupS sG1) //.
    by apply/trivgP; rewrite -regR setSI.
  by apply: leq_trans leKm; apply: proper_card.
have cK'K': abelian K^`(1).
  exact: ltK_abelian (gFnorm_trans _ nKR) (sol_der1_proper solK _ ntK).
pose fixG := rfix_mx rG; pose NRmod N (U : 'M_n) := N <*> R \subset rstabs rG U.
have dx_modK_rfix (N : {group gT}) U V:
    N \subset K -> R \subset 'N(N) -> NRmod N U -> NRmod N V ->
  mxdirect (U + V) -> (U <= fixG N)%MS || (V <= fixG N)%MS.
- move=> sNK nNR nUNR nVNR dxUV.
  have [-> | ntN] := eqsVneq N 1; first by rewrite -rfix_mx_rstabC sub1G.
  have sNRG: N <*> R \subset G by rewrite join_subG (subset_trans sNK).
  pose rNR := subg_repr rG sNRG.
  have nfixU W: NRmod N W -> ~~ (W <= fixG N)%MS -> (fixG R <= W)%MS.
    move=> nWN not_cWN; rewrite (sameP capmx_idPr eqmxP).
    rewrite -(geq_leqif (mxrank_leqif_eq (capmxSr _ _))) fixRlin lt0n.
    rewrite mxrank_eq0 -(in_submodK (capmxSl _ _)) val_submod_eq0.
    have modW: mxmodule rNR W by rewrite /mxmodule rstabs_subg subsetI subxx.
    rewrite -(eqmx_eq0 (rfix_submod modW _)) ?joing_subr //.
    apply: Frobenius_rfix_compl (pgroupS (subset_trans sNK sKG) F'G) _.
      apply/Frobenius_semiregularP=> // [|x Rx].
        by rewrite sdprodEY //; apply/trivgP; rewrite -tiKR setSI.
      by apply/trivgP; rewrite -regR /= -cent_cycle defR ?setSI.
    by rewrite rker_submod rfix_mx_rstabC ?joing_subl.
  have: fixG R != 0 by rewrite -mxrank_eq0 fixRlin.
  apply: contraR; case/norP=> not_fixU not_fixW.
  by rewrite -submx0 -(mxdirect_addsP dxUV) sub_capmx !nfixU.
have redG := mx_Maschke rG F'G.
wlog [U simU nfixU]: / exists2 U, mxsimple rG U & ~~ (U <= fixG K)%MS.
  move=> IH; wlog [I U /= simU sumU _]: / mxsemisimple rG 1%:M.
    exact: (mx_reducible_semisimple (mxmodule1 _) redG).
  have [i nfixU | fixK] := pickP (fun i => ~~ (U i <= fixG K)%MS).
    by apply: IH; exists (U i).
  rewrite gFsub_trans // rfix_mx_rstabC // -sumU.
  by apply/sumsmx_subP=> i _; apply/idPn; rewrite fixK.
have [modU ntU minU] := simU; pose rU := submod_repr modU.
have irrU: mx_irreducible rU by apply/submod_mx_irr.
have [W modW sumUW dxUW] := redG U modU (submx1 U).
have cWK: (W <= fixG K)%MS.
  have:= dx_modK_rfix _ _ _ (subxx _) nKR _ _ dxUW.
  by rewrite /NRmod /= norm_joinEr // defKR (negPf nfixU); apply.
have nsK'G: K^`(1) <| G by rewrite gFnormal_trans.
have [sK'G nK'G] := andP nsK'G.
suffices nregK'U: (rfix_mx rU K^`(1))%MS != 0.
  rewrite rfix_mx_rstabC ?normal_sub // -sumUW addsmx_sub andbC.
  rewrite (submx_trans cWK) ?rfix_mxS ?der_sub //= (sameP capmx_idPl eqmxP).
  rewrite minU ?capmxSl ?capmx_module ?normal_rfix_mx_module //.
  apply: contra nregK'U => cUK'; rewrite (eqmx_eq0 (rfix_submod _ _)) //.
  by rewrite (eqP cUK') linear0.
pose rK := subg_repr rU (normal_sub nsKG); set p := #|R| in p_pr.
wlog sK: / socleType rK by apply: socle_exists.
have [i _ def_sK]: exists2 i, i \in setT & [set: sK] = orbit 'Cl G i.
  exact/imsetP/Clifford_atrans.
have card_sK: #|[set: sK]| =  #|G : 'C[i | 'Cl]|.
  by rewrite def_sK card_orbit_in ?indexgI.
have ciK: K \subset 'C[i | 'Cl].
  apply: subset_trans (astabS _ (subsetT _)).
  by apply: subset_trans (Clifford_astab _); apply: joing_subl.
pose M := socle_base i; have simM: mxsimple rK M := socle_simple i.
have [sKp | sK1 {ciK card_sK}]: #|[set: sK]| = p \/ #|[set: sK]| = 1%N.
- apply/pred2P; rewrite orbC card_sK; case/primeP: p_pr => _; apply.
  by rewrite (_ : p = #|G : K|) ?indexgS // -divgS // -(sdprod_card defG) mulKn.
- have{def_sK} def_sK: [set: sK] = orbit 'Cl R i.
    apply/eqP; rewrite eq_sym -subTset def_sK -[G in orbit _ G i]defKR.
    apply/subsetP=> _ /imsetP[_ /imset2P[y z /(subsetP ciK)ciy Rz ->] ->].
    rewrite !(inE, sub1set) in ciy; have{ciy}[Gy /eqP-ciy]:= andP ciy.
    by rewrite actMin ?(subsetP sRG z Rz) // ciy mem_orbit.
  have inj_i: {in R &, injective ('Cl%act i)}.
    apply/dinjectiveP/card_uniqP; rewrite size_map -cardE -/p.
    by rewrite -sKp def_sK /orbit [in _ @: _]unlock cardsE.
  pose sM := (\sum_(y in R) M *m rU y)%MS.
  have dxM: mxdirect sM.
    apply/mxdirect_sumsP=> y Ry; have Gy := subsetP sRG y Ry.
    pose j := 'Cl%act i y.
    apply/eqP; rewrite -submx0 -{2}(mxdirect_sumsP (Socle_direct sK) j) //.
    rewrite capmxS ?val_Clifford_act // ?submxMr ?component_mx_id //.
    apply/sumsmx_subP => z; case/andP=> Rz ne_z_y; have Gz := subsetP sRG z Rz.
    rewrite (sumsmx_sup ('Cl%act i z)) ?(inj_in_eq inj_i) //.
    by rewrite val_Clifford_act // ?submxMr // ?component_mx_id.
  pose inCR := \sum_(x in R) rU x.
  have im_inCR: (inCR <= rfix_mx rU R)%MS.
    apply/rfix_mxP=> x Rx; have Gx := subsetP sRG x Rx.
    rewrite {2}[inCR](reindex_astabs 'R x) ?astabsR //= mulmx_suml.
    by apply: eq_bigr => y; move/(subsetP sRG)=> Gy; rewrite repr_mxM.
  pose inM := proj_mx M (\sum_(x in R | x != 1) M *m rU x)%MS.
  have dxM1 := mxdirect_sumsP dxM _ (group1 R).
  rewrite repr_mx1 mulmx1 in dxM1.
  have inCR_K: M *m inCR *m inM = M.
    rewrite mulmx_sumr (bigD1 1) //= repr_mx1 mulmx1 mulmxDl proj_mx_id //.
    by rewrite proj_mx_0 ?addr0 // summx_sub_sums.
  have [modM ntM _] := simM.
  have linM: \rank M = 1%N.
    apply/eqP; rewrite eqn_leq lt0n mxrank_eq0 ntM andbT.
    rewrite -inCR_K; apply: leq_trans (mxrankM_maxl _ _) _.
    apply: leq_trans (mxrankS (mulmx_sub _ im_inCR)) _.
    rewrite rfix_submod //; apply: leq_trans (mxrankM_maxl _ _) _.
    by rewrite -fixRlin mxrankS ?capmxSr.
  apply: contra (ntM); move/eqP; rewrite -submx0 => <-.
  by rewrite -(rfix_mx_rstabC rK) ?der_sub // -(rker_submod modM) rker_linear.
have{sK i M simM sK1 def_sK} irrK: mx_irreducible rK.
  have cycGq: cyclic (G / K) by rewrite -defKR quotientMidl quotient_cyclic.
  apply: (mx_irr_prime_index closF irrU cycGq simM) => x Gx /=.
  apply: (component_mx_iso simM); first exact: Clifford_simple.
  have jP: component_mx rK (M *m rU x) \in socle_enum sK.
    exact/component_socle/Clifford_simple.
  pose j := PackSocle jP; apply: submx_trans (_ : j <= _)%MS.
    by rewrite PackSocleK component_mx_id //; apply: Clifford_simple.
  have def_i: [set i] == [set: sK] by rewrite eqEcard subsetT cards1 sK1.
  by rewrite ((j =P i) _) // -in_set1 (eqP def_i) inE.
pose G' := K^`(1) <*> R.
have sG'G: G' \subset G by rewrite join_subG sK'G.
pose rG' := subg_repr rU sG'G.
wlog irrG': / mx_irreducible rG'.
  move=> IH; wlog [M simM sM1]: / exists2 M, mxsimple rG' M & (M <= 1%:M)%MS.
    by apply: mxsimple_exists; rewrite ?mxmodule1; case: irrK.
  have [modM ntM _] := simM.
  have [M' modM' sumM dxM] := mx_Maschke rG' (pgroupS sG'G F'G) modM sM1.
  wlog{IH} ntM': / M' != 0.
    case: eqP sumM => [-> M1 _ | _ _ -> //]; apply: IH.
    by apply: mx_iso_simple simM; apply: eqmx_iso; rewrite addsmx0_id in M1.
  suffices: (K^`(1) \subset rstab rG' M) || (K^`(1) \subset rstab rG' M').
    rewrite !rfix_mx_rstabC ?joing_subl //; rewrite -!submx0 in ntM ntM' *.
    by case/orP; move/submx_trans=> sM; apply: (contra (sM _ _)).
  rewrite !rstab_subg !rstab_submod !subsetI joing_subl !rfix_mx_rstabC //.
  rewrite /mxmodule !rstabs_subg !rstabs_submod !subsetI !subxx in modM modM'.
  do 2!rewrite orbC -genmxE.
  rewrite dx_modK_rfix // /NRmod ?(eqmx_rstabs _ (genmxE _)) ?der_sub //.
    exact: subset_trans sRG nK'G.
  apply/mxdirect_addsP; apply/eqP; rewrite -genmx_cap (eqmx_eq0 (genmxE _)).
  rewrite -(in_submodK (submx_trans (capmxSl _ _) (val_submodP _))).
  rewrite val_submod_eq0 in_submodE -submx0 (submx_trans (capmxMr _ _ _)) //.
  by rewrite -!in_submodE !val_submodK (mxdirect_addsP dxM).
have nsK'K: K^`(1) <| K by apply: der_normal.
pose rK'K := subg_repr rK (normal_sub nsK'K).
have irrK'K: mx_absolutely_irreducible rK'K.
  wlog sK'K: / socleType rK'K by apply: socle_exists.
  have sK'_dv_K: #|[set: sK'K]| %| #|K|.
    exact: atrans_dvd_in (Clifford_atrans _ _).
  have nsK'G': K^`(1) <| G' := normalS (joing_subl _ _) sG'G nsK'G.
  pose rK'G' := subg_repr rG' (normal_sub nsK'G').
  wlog sK'G': / socleType rK'G' by apply: socle_exists.
  have coKp: coprime #|K| p := Frobenius_coprime frobG.
  have nK'R := subset_trans sRG nK'G.
  have sK'_dv_p: #|[set: sK'G']| %| p.
    suffices: #|G' : 'C([set: sK'G'] | 'Cl)| %| #|G' : K^`(1)|.
      rewrite -(divgS (joing_subl _ _)) /= {2}norm_joinEr //.
      rewrite coprime_cardMg ?(coprimeSg (normal_sub nsK'K)) //.
      rewrite mulKn ?cardG_gt0 // -indexgI; apply: dvdn_trans.
      exact: atrans_dvd_index_in (Clifford_atrans _ _).
    rewrite indexgS //; apply: subset_trans (Clifford_astab sK'G').
    exact: joing_subl.
  have eq_sK': #|[set: sK'K]| = #|[set: sK'G']|.
    rewrite !cardsT !cardE -!(size_map (fun i => socle_val i)).
    apply: perm_eq_size.
    rewrite uniq_perm_eq 1?(map_inj_uniq val_inj) 1?enum_uniq // => V.
    apply/mapP/mapP=> [] [i _ ->{V}].
      exists (PackSocle (component_socle sK'G' (socle_simple i))).
        by rewrite mem_enum.
      by rewrite PackSocleK.
    exists (PackSocle (component_socle sK'K (socle_simple i))).
      by rewrite mem_enum.
    by rewrite PackSocleK.
  have [i def_i]: exists i, [set: sK'G'] = [set i].
    apply/cards1P; rewrite -dvdn1 -{7}(eqnP coKp) dvdn_gcd.
    by rewrite -{1}eq_sK' sK'_dv_K sK'_dv_p.
  pose M := socle_base i; have simM : mxsimple rK'G' M := socle_simple i.
  have cycGq: cyclic (G' / K^`(1)).
    by rewrite /G' joingC quotientYidr ?quotient_cyclic.
  apply closF; apply: (mx_irr_prime_index closF irrG' cycGq simM) => x K'x /=.
  apply: (component_mx_iso simM); first exact: Clifford_simple.
  have jP: component_mx rK'G' (M *m rG' x) \in socle_enum sK'G'.
    exact/component_socle/Clifford_simple.
  pose j := PackSocle jP; apply: submx_trans (_ : j <= _)%MS.
    by rewrite PackSocleK component_mx_id //; apply: Clifford_simple.
  by rewrite ((j =P i) _) // -in_set1 -def_i inE.
have linU: \rank U = 1%N by apply/eqP; rewrite abelian_abs_irr in irrK'K.
case: irrU => _ nz1 _; apply: contra nz1; move/eqP=> fix0.
by rewrite -submx0 -fix0 -(rfix_mx_rstabC rK) ?der_sub // rker_linear.
Qed.

(* Internal action version of B & G, Theorem 3.5. *)
Theorem Frobenius_prime_cent_prime k gT (G K R V : {group gT}) :
    solvable G -> K ><| R = G -> prime #|R| -> 'C_K(R) = 1 -> 
    k.-abelem V -> G \subset 'N(V) -> k^'.-group G -> #|'C_V(R)| = k ->
  K^`(1) \subset 'C_K(V).
Proof.
move=> solG defG prR regRK abelV nVG k'G primeRV.
have [_ sRG _ nKR _] := sdprod_context defG; rewrite subsetI der_sub.
have [-> | ntV] := eqsVneq V 1; first exact: cents1.
pose rV := abelem_repr abelV ntV nVG.
apply: subset_trans (_ : rker rV \subset _); last first.
  by rewrite rker_abelem subsetIr.
have k_pr: prime k by case/pgroup_pdiv: (abelem_pgroup abelV).
apply: (Frobenius_prime_rfix1 defG) => //.
  by rewrite (eq_pgroup G (eq_negn (charf_eq (char_Fp k_pr)))).
apply/eqP; rewrite rfix_abelem // -(eqn_exp2l _ _ (prime_gt1 k_pr)).
rewrite -{1}(card_Fp k_pr) -card_rowg rowg_mxK.
by rewrite card_injm ?abelem_rV_injm ?subsetIl ?primeRV.
Qed.

Section Theorem_3_6.
(* Limit the scope of the FiniteModule notations *)
Import FiniteModule.

(* This is B & G, Theorem 3.6. *)
Theorem odd_sdprod_Zgroup_cent_prime_plength1 p gT (G H R R0 : {group gT}) :
    solvable G -> odd #|G| -> H ><| R = G -> coprime #|H| #|R| ->
    R0 \subset R -> prime #|R0| -> Zgroup 'C_H(R0) ->
  p.-length_1 [~: H, R].
Proof.
move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G H R R0 *.
rewrite ltnS; move oR0: #|R0| => r leGn solG oddG defG coHR sR0R r_pr ZgrCHR0.
have rR0: r.-group R0 by rewrite /pgroup oR0 pnat_id.
have [nsHG sRG mulHR nHR tiHR]:= sdprod_context defG.
have [sHG nHG] := andP nsHG; have solH := solvableS sHG solG.
have IHsub (H1 R1 : {group gT}):
    H1 \subset H -> H1 * R1 \subset 'N(H1) -> R0 \subset R1 -> R1 \subset R ->
  (#|H1| < #|H|) || (#|R1| < #|R|) -> p.-length_1 [~: H1, R1].
- move=> sH1 nH1 sR01 sR1 ltG1; set G1 := H1 <*> R1.
  have coHR1: coprime #|H1| #|R1| by rewrite (coprimeSg sH1) // (coprimegS sR1).
  have defG1: H1 ><| R1 = G1.
    by rewrite sdprodEY ?coprime_TIg ?(subset_trans (mulG_subr H1 R1)).
  have sG1: G1 \subset G by rewrite join_subG -mulG_subG -mulHR mulgSS.
  have{ltG1} ltG1n: #|G1| < n.
    rewrite (leq_trans _ leGn) // -(sdprod_card defG1) -(sdprod_card defG).
    have leqifS := leqif_geq (subset_leq_card _).
    rewrite ltn_neqAle !(leqif_mul (leqifS _ _ _ sH1) (leqifS _ _ _ sR1)).
    by rewrite muln_eq0 !negb_or negb_and -!ltnNge ltG1 -!lt0n !cardG_gt0.
  apply: IHn defG1 _ sR01 _ _; rewrite ?oR0 ?(solvableS sG1) ?(oddSg sG1) //.
  exact: ZgroupS (setSI _ sH1) ZgrCHR0.
without loss defHR: / [~: H, R] = H; last rewrite defHR.
  have sHR_H: [~: H, R] \subset H by rewrite commg_subl.
  have:= sHR_H; rewrite subEproper; case/predU1P=> [-> -> //|ltHR_H _].
  rewrite -coprime_commGid // IHsub 1?proper_card //.
  by apply: subset_trans (commg_norm H R); rewrite norm_joinEr ?mulSg.
have{n leGn IHn tiHR} IHquo (X : {group gT}):
  X :!=: 1 -> X \subset H -> G \subset 'N(X) -> p.-length_1 (H / X).
- move=> ntX sXH nXG; have nXH := subset_trans sHG nXG.
  have nXR := subset_trans sRG nXG; have nXR0 := subset_trans sR0R nXR.
  rewrite -defHR quotientE morphimR // -!quotientE.
  have ltGbn: #|G / X| < n.
    exact: leq_trans (ltn_quotient ntX (subset_trans sXH sHG)) _.
  have defGb: (H / X) ><| (R / X) = G / X by apply: quotient_coprime_sdprod.
  have pr_R0b: prime #|R0 / X|.
    have tiXR0: X :&: R0 = 1 by apply/trivgP; rewrite -tiHR setISS.
    by rewrite card_quotient // -indexgI setIC tiXR0 indexg1 oR0.
  have solGb: solvable (G / X) by apply: quotient_sol.
  have coHRb: coprime #|H / X| #|R / X| by apply: coprime_morph.
  apply: IHn defGb coHRb _ pr_R0b _; rewrite ?quotientS ?quotient_odd //.
  by rewrite -coprime_quotient_cent ?(coprimegS sR0R) // morphim_Zgroup.
without loss Op'H: / 'O_p^'(H) = 1.
  have [_ -> // | ntO _] := eqVneq 'O_p^'(H) 1.
  suffices: p.-length_1 (H / 'O_p^'(H)).
    by rewrite p'quo_plength1 ?pcore_normal ?pcore_pgroup.
  apply: IHquo => //; first by rewrite normal_sub ?pcore_normal.
  by rewrite normal_norm // gFnormal_trans.
move defV: 'F(H)%G => V.
have charV: V \char H by rewrite -defV Fitting_char.
have /andP[sVH nVH]: V <| H := char_normal charV.
have nsVG: V <| G := char_normal_trans charV nsHG.
have [_ nVG] := andP nsVG; have nVR: R \subset 'N(V) := subset_trans sRG nVG.
without loss ntV: / V :!=: 1.
  by rewrite -defV trivg_Fitting //; case: eqP => [|_] ->; rewrite ?plength1_1.
have scVHV: 'C_H(V) \subset V by rewrite -defV cent_sub_Fitting.
have{defV Op'H} defV: 'O_p(H) = V by rewrite -(Fitting_eq_pcore Op'H) -defV.
have pV: p.-group V by rewrite -defV pcore_pgroup.
have [p_pr p_dv_V _] := pgroup_pdiv pV ntV.
have p'r: r != p.
  rewrite eq_sym -dvdn_prime2 // -prime_coprime // (coprime_dvdl p_dv_V) //.
  by rewrite -oR0 (coprimegS sR0R) // (coprimeSg sVH).
without loss{charV} abelV: / p.-abelem V; last have [_ cVV eV] := and3P abelV.
  move/implyP; rewrite implybE -trivg_Phi //; case/orP=> // ntPhi.
  have charPhi: 'Phi(V) \char H := gFchar_trans _ charV.
  have nsPhiH := char_normal charPhi; have [sPhiH nPhiH] := andP nsPhiH.
  have{charPhi} nPhiG: G \subset 'N('Phi(V)):= char_norm_trans charPhi nHG.
  rewrite -(pquo_plength1 nsPhiH) 1?IHquo ?(pgroupS (Phi_sub _)) //.
  have [/= W defW sPhiW nsWH] := inv_quotientN nsPhiH (pcore_normal p^' _).
  have p'Wb: p^'.-group (W / 'Phi(V)) by rewrite -defW pcore_pgroup.
  have{p'Wb} tiWb := coprime_TIg (pnat_coprime (quotient_pgroup _ _) p'Wb).
  suffices pW: p.-group W by rewrite -(tiWb W pW) setIid.
  apply/pgroupP=> q q_pr; case/Cauchy=> // x Wx ox; apply: wlog_neg => q'p.
  suffices Vx: x \in V by rewrite (pgroupP pV) // -ox order_dvdG.
  have [sWH nWH] := andP nsWH; rewrite (subsetP scVHV) // inE (subsetP sWH) //=.
  have coVx: coprime #|V| #[x] by rewrite ox (pnat_coprime pV) // pnatE.
  rewrite -cycle_subG (coprime_cent_Phi pV coVx) //.
  have: V :&: W \subset 'Phi(V); last apply: subset_trans.
    rewrite -quotient_sub1; last by rewrite subIset ?(subset_trans sWH) ?orbT.
    by rewrite quotientIG ?tiWb.
  rewrite commg_subI //; first by rewrite subsetI subxx (subset_trans sVH).
  by rewrite cycle_subG inE Wx (subsetP nVH) // (subsetP sWH).
have{scVHV} scVH: 'C_H(V) = V by apply/eqP; rewrite eqEsubset scVHV subsetI sVH.
without loss{IHquo} indecomposableV: / forall U W,
  U \x W = V -> G \subset 'N(U) :&: 'N(W) -> U = 1 \/ U = V.
- pose decV UW := let: (U, W) := UW in
    [&& U \x W == V, G \subset 'N(U) :&: 'N(W), U != 1 & W != 1].
  case: (pickP decV) => [[A B /=] | indecV]; last first.
    apply=> U W defUW nUW_G; have:= indecV (U, W); rewrite /= -defUW nUW_G eqxx.
    by rewrite -negb_or; case/pred2P=> ->; [left | right; rewrite dprodg1].
  rewrite subsetI -!andbA => /and5P[/eqP/dprodP[[U W -> ->{A B}]]].
  move=> defUW _ tiUW nUG nWG ntU ntW _.
  have [sUH sWH]: U \subset H /\ W \subset H.
    by apply/andP; rewrite -mulG_subG defUW.
  have [nsUH nsWH]: U <| H /\ W <| H.
    by rewrite /normal !(subset_trans sHG) ?andbT.
  by rewrite -(quo2_plength1 _ nsUH nsWH) ?tiUW ?IHquo.
have nsFb: 'F(H / V) <| G / V by rewrite gFnormal_trans ?quotient_normal.
have{nsVG nsFb} [/= U defU sVU nsUG] := inv_quotientN nsVG nsFb.
have{nsUG} [sUG nUG] := andP nsUG.
have [solU nVU] := (solvableS sUG solG, subset_trans sUG nVG).
have sUH: U \subset H by rewrite -(quotientSGK nVU sVH) -defU Fitting_sub.
have [K hallK nKR]: exists2 K : {group gT}, p^'.-Hall(U) K & R \subset 'N(K).
  by apply: coprime_Hall_exists; rewrite ?(coprimeSg sUH) ?(subset_trans sRG).
have [sKU p'K _] := and3P hallK; have{sUG} sKG := subset_trans sKU sUG.
have coVK: coprime #|V| #|K| := pnat_coprime pV p'K.
have [sKH nVK] := (subset_trans sKU sUH, subset_trans sKU nVU).
have{defV} p'Ub: p^'.-group (U / V).
  rewrite -defU -['F(H / V)](nilpotent_pcoreC p (Fitting_nil _)) /=.
  by rewrite p_core_Fitting -defV trivg_pcore_quotient dprod1g pcore_pgroup.
have{p'Ub} sylV: p.-Sylow(U) V by rewrite /pHall sVU pV -card_quotient.
have{sKU} mulVK: V * K = U.
  apply/eqP; rewrite eqEcard mul_subG //= coprime_cardMg //.
  by rewrite (card_Hall sylV) (card_Hall hallK) partnC.
have [sKN sNH]: K \subset 'N_H(K) /\ 'N_H(K) \subset H.
  by rewrite subsetIl subsetI sKH normG.
have [solN nVN] := (solvableS sNH solH, subset_trans sNH nVH).
have{solU hallK sUH nUG} defH: V * 'N_H(K) = H.
  have nsUH: U <| H by apply/andP; rewrite (subset_trans sHG).
  by rewrite -(mulSGid sKN) mulgA mulVK (Hall_Frattini_arg solU nsUH hallK).
have [P sylP nPR]: exists2 P : {group _}, p.-Sylow('N_H(K)) P & R \subset 'N(P).
  apply: coprime_Hall_exists (coprimeSg sNH coHR) solN.
  by rewrite normsI ?norms_norm.
have [sPN pP _]: [/\ P \subset 'N_H(K), p.-group P & _] := and3P sylP.
have [sPH nKP]: P \subset H /\ P \subset 'N(K) by apply/andP; rewrite -subsetI.
have nVP := subset_trans sPH nVH.
have coKP: coprime #|K| #|P| by rewrite coprime_sym (pnat_coprime pP).
have{sylP} sylVP: p.-Sylow(H) (V <*> P).
  rewrite pHallE /= norm_joinEr ?mul_subG //= -defH -!LagrangeMl.
  rewrite partnM // part_pnat_id // -!card_quotient //.
  by apply/eqP; congr (_ * _)%N; apply: card_Hall; apply: quotient_pHall.
have [trKP | {sylV sVU nVU}ntKP] := eqVneq [~: K, P] 1.
  suffices sylVH: p.-Sylow(H) V.
    rewrite p_elt_gen_length1 // (_ : p_elt_gen p H = V).
      rewrite /pHall pcore_sub pcore_pgroup /= pnatNK.
      by apply: pnat_dvd pV; apply: dvdn_indexg.
    rewrite -(genGid V) -(setIidPr sVH); congr <<_>>; apply/setP=> x.
    rewrite !inE; apply: andb_id2l => Hx.
    by rewrite (mem_normal_Hall sylVH) /normal ?sVH.
  suffices sPV: P \subset V by rewrite -(joing_idPl sPV).
  suffices sPU: P \subset U by rewrite (sub_normal_Hall sylV) //; apply/andP.
  have cUPb: P / V \subset 'C_(H / V)(U / V).
    rewrite subsetI morphimS // -mulVK quotientMidl quotient_cents2r //.
    by rewrite commGC trKP sub1G.
  rewrite -(quotientSGK nVP sVU) (subset_trans cUPb) //.
  by rewrite -defU cent_sub_Fitting ?quotient_sol.
have{sylVP} dxV: [~: V, K] \x 'C_V(K) = V by apply: coprime_abelian_cent_dprod.
have tiVsub_VcK: 'C_V(K) = 1 \/ 'C_V(K) = V.
  apply: (indecomposableV _  [~: V, K]); first by rewrite dprodC.
  rewrite -mulHR -defH -mulgA mul_subG // subsetI.
    by rewrite commg_norml cents_norm // centsC subIset // -abelianE cVV.
  have nK_NR: 'N_H(K) * R \subset 'N(K) by rewrite mul_subG ?subsetIr.
  have nV_NR: 'N_H(K) * R \subset 'N(V) by rewrite mul_subG.
  by rewrite normsR // normsI ?norms_cent.
have{tiVsub_VcK dxV} [defVK tiVcK]: [~: V, K] = V /\ 'C_V(K) = 1.
  have [tiVcK | eqC] := tiVsub_VcK; first by rewrite -{2}dxV // tiVcK dprodg1.
  rewrite (card1_trivg (pnat_1 (pgroupS _ pV) p'K)) ?comm1G ?eqxx // in ntKP.
  by rewrite -scVH subsetI sKH centsC -eqC subsetIr.
have eqVncK: 'N_V(K) = 'C_V(K) := coprime_norm_cent nVK (pnat_coprime pV p'K).
have{eqVncK} tiVN: V :&: 'N_H(K) = 1 by rewrite setIA (setIidPl sVH) eqVncK.
have{sPN} tiVP: V :&: P = 1 by apply/trivgP; rewrite -tiVN setIS.
have{U defU mulVK} defK: 'F('N_H(K)) = K.
  have [injV imV] := isomP (quotient_isom nVN tiVN).
  rewrite -(im_invm injV) -injm_Fitting ?injm_invm //= {2}imV /=.
  rewrite -quotientMidl defH defU -mulVK quotientMidl morphim_invmE.
  by rewrite morphpre_restrm quotientK // -group_modr // setIC tiVN mul1g.
have scKH: 'C_H(K) \subset K.
  rewrite -{2}defK; apply: subset_trans (cent_sub_Fitting _) => //.
  by rewrite defK subsetI subsetIr setIS // cent_sub.
have{nVN} ntKR0: [~: K, R0] != 1.
  rewrite (sameP eqP commG1P); apply: contra ntKP => cR0K.
  have ZgrK: Zgroup K by apply: ZgroupS ZgrCHR0; rewrite subsetI sKH.
  have{ZgrK} cycK: cyclic K by rewrite nil_Zgroup_cyclic // -defK Fitting_nil.
  have{cycK} sNR_K: [~: 'N_H(K), R] \subset K.
    apply: subset_trans scKH; rewrite subsetI; apply/andP; split.
      by rewrite (subset_trans (commSg R sNH)) // commGC commg_subr.
    suffices: 'N(K)^`(1) \subset 'C(K).
      by apply: subset_trans; rewrite commgSS ?subsetIr.
    rewrite der1_min ?cent_norm //= -ker_conj_aut (isog_abelian (first_isog _)).
    exact: abelianS (Aut_conj_aut K 'N(K)) (Aut_cyclic_abelian cycK).
  suffices sPV: P \subset V by rewrite -(setIidPr sPV) tiVP commG1.
  have pPV: p.-group (P / V) := quotient_pgroup V pP.
  rewrite -quotient_sub1 // subG1 (card1_trivg (pnat_1 pPV _)) //.
  apply: pgroupS (quotient_pgroup V p'K).
  apply: subset_trans (quotientS V sNR_K).
  by rewrite quotientR // -quotientMidl defH -quotientR ?defHR ?quotientS.
have nKR0: R0 \subset 'N(K) := subset_trans sR0R nKR.
have mulKR0: K * R0 = K <*> R0 by rewrite norm_joinEr.
have sKR0_G : K <*> R0 \subset G by rewrite -mulKR0 -mulHR mulgSS.
have nV_KR0: K <*> R0 \subset 'N(V) := subset_trans sKR0_G nVG.
have solKR0: solvable (K <*> R0) by apply: solvableS solG.
have coKR0: coprime #|K| #|R0| by rewrite (coprimeSg sKH) ?(coprimegS sR0R).
have r'K: r^'.-group K.
  by rewrite /pgroup p'natE -?prime_coprime // coprime_sym -oR0.
have tiKcV: 'C_K(V) = 1.
  by apply/trivgP; rewrite -tiVN -{2}scVH -setIIr setICA setIC setSI.
have tiKR0cV: 'C_(K <*> R0)(V) = 1.
  set C := 'C_(K <*> R0)(V); apply/eqP; apply: contraR ntKR0 => ntC.
  have nC_KR0: K <*> R0 \subset 'N(C) by rewrite normsI ?normG ?norms_cent.
  rewrite -subG1 -(coprime_TIg coKR0) commg_subI ?subsetI ?subxx //=.
  suff defC: C == R0 by rewrite -(eqP defC) (subset_trans (joing_subl K R0)).
  have sC_R0: C \subset R0.
    rewrite -[C](coprime_mulG_setI_norm mulKR0) ?norms_cent //= tiKcV mul1g.
    apply: subsetIl.
  rewrite eqEsubset sC_R0; apply: contraR ntC => not_sR0C.
  by rewrite -(setIidPr sC_R0) prime_TIg ?oR0.
have{nKR0 mulKR0 sKR0_G solKR0 nV_KR0} oCVR0: #|'C_V(R0)| = p.
  case: (eqVneq 'C_V(R0) 1) => [tiVcR0 | ntCVR0].
    case/negP: ntKR0; rewrite -subG1/= commGC -tiKcV.
    have defKR0: K ><| R0 = K <*> R0 by rewrite sdprodE ?coprime_TIg.
    have odd_KR0: odd #|K <*> R0| := oddSg sKR0_G oddG.
    apply: odd_prime_sdprod_abelem_cent1 abelV nV_KR0 _ _; rewrite // ?oR0 //=.
    by rewrite -mulKR0 pgroupM p'K /pgroup oR0 pnatE.
  have [x defC]: exists x, 'C_V(R0) = <[x]>.
    have ZgrC: Zgroup 'C_V(R0) by apply: ZgroupS ZgrCHR0; apply: setSI.
    apply/cyclicP; apply: (forall_inP ZgrC); apply/SylowP; exists p => //.
    by rewrite /pHall subxx indexgg (pgroupS (subsetIl V _)).
  rewrite defC; apply: nt_prime_order => //; last by rewrite -cycle_eq1 -defC.
  by rewrite (exponentP eV) // -cycle_subG -defC subsetIl.
have tiPcR0: 'C_P(R0) = 1.
  rewrite -(setIidPl (joing_subl P V)) setIIl TI_Ohm1 //=.
  set C := 'C_(P <*> V)(R0); suffices <-: 'C_V(R0) = 'Ohm_1(C).
    by rewrite setIC -setIIl tiVP (setIidPl (sub1G _)).
  have pPV: p.-group (P <*> V) by rewrite norm_joinEl // pgroupM pP.
  have pC: p.-group C := pgroupS (subsetIl _ _) pPV.
  have abelCVR0: p.-abelem 'C_V(R0) by rewrite prime_abelem ?oCVR0.
  have sCV_C: 'C_V(R0) \subset C by rewrite setSI ?joing_subr.
  apply/eqP; rewrite eqEcard -(Ohm1_id abelCVR0) OhmS //=.
  have [-> | ntC] := eqVneq C 1; first by rewrite subset_leq_card ?OhmS ?sub1G.
  rewrite (Ohm1_id abelCVR0) oCVR0 (Ohm1_cyclic_pgroup_prime _ pC) //=.
  have ZgrC: Zgroup C by rewrite (ZgroupS _ ZgrCHR0) ?setSI // join_subG sPH.
  apply: (forall_inP ZgrC); apply/SylowP; exists p => //.
  by apply/pHallP; rewrite part_pnat_id.
have defP: [~: P, R0] = P.
  have solvP := pgroup_sol pP; have nPR0 := subset_trans sR0R nPR.
  have coPR0: coprime #|P| #|R0| by rewrite (coprimeSg sPH) ?(coprimegS sR0R).
  by rewrite -{2}(coprime_cent_prod nPR0) // tiPcR0 mulg1.
have{IHsub nVH} IHsub: forall X : {group gT},
  P <*> R0 \subset 'N(X) -> X \subset K ->
  (#|V <*> X <*> P| < #|H|) || (#|R0| < #|R|) -> [~: X, P] = 1.
- move=> X; rewrite join_subG; case/andP=> nXP nXR0 sXK.
  set H0 := V <*> X <*> P => ltG0G; have sXH := subset_trans sXK sKH.
  have sXH0: X \subset H0 by rewrite /H0 joingC joingA joing_subr.
  have sH0H: H0 \subset H by rewrite !join_subG sVH sXH.
  have nH0R0: R0 \subset 'N(H0).
    by rewrite 2?normsY ?nXR0 ?(subset_trans sR0R) // (subset_trans sRG).
  have Op'H0: 'O_p^'(H0) = 1.
    have [sOp' nOp'] := andP (pcore_normal _ _ : 'O_p^'(H0) <| H0).
    have p'Op': p^'.-group 'O_p^'(H0) by apply: pcore_pgroup.
    apply: card1_trivg (pnat_1 (pgroupS _ pV) p'Op').
    rewrite -scVH subsetI (subset_trans sOp') //= centsC; apply/setIidPl.
    rewrite -coprime_norm_cent ?(pnat_coprime pV p'Op') //.
      by rewrite (setIidPl (subset_trans _ nOp')) // /H0 -joingA joing_subl.
    exact: subset_trans (subset_trans sH0H nVH).
  have Op'HR0: 'O_p^'([~: H0, R0]) = 1.
    apply/trivgP; rewrite -Op'H0 pcore_max ?pcore_pgroup // gFnormal_trans //.
    by rewrite /(_ <| _) commg_norml andbT commg_subl.
  have{ltG0G IHsub} p1_HR0: p.-length_1 [~: H0, R0].
    by apply: IHsub ltG0G => //=; rewrite mul_subG ?normG.
  have{p1_HR0} sPOpHR0: P \subset 'O_p([~: H0, R0]).
    rewrite sub_Hall_pcore //; last by rewrite -defP commSg ?joing_subr.
    rewrite /pHall pcore_sub pcore_pgroup /= -(pseries_pop2 _ Op'HR0).
    rewrite -card_quotient ?normal_norm ?pseries_normal // -/(pgroup _ _).
    by rewrite -{1}((_ :=P: _) p1_HR0) (quotient_pseries [::_;_]) pcore_pgroup.
  apply/trivgP; have <-: K :&: 'O_p([~: H0, R0]) = 1.
    by rewrite setIC coprime_TIg // (pnat_coprime (pcore_pgroup p _)).
  by rewrite commg_subI // subsetI ?sPOpHR0 ?sXK //= gFnorm_trans // normsRl.
have{defH sR0R} [defH defR0]: V * K * P = H /\ R0 :=: R.
  suffices: (V * K * P == H) && (R0 :==: R) by do 2!case: eqP => // ->.
  apply: contraR ntKP; rewrite -subG1 !eqEcard sR0R ?mul_subG //= negb_and.
  rewrite -!ltnNge -!norm_joinEr // 1?normsY //; move/IHsub=> -> //.
  by rewrite join_subG nKP (subset_trans sR0R).
move: IHsub defP oR0 rR0 ZgrCHR0 coKR0 ntKR0 tiKR0cV oCVR0 tiPcR0.
rewrite {R0}defR0 ltnn => IHsub defP oR rR ZgrCHR coKR ntKR tiKRcV oCVR tiPcR.
have mulVK: V * K = V <*> K by rewrite norm_joinEr.
have oVK: #|V <*> K| = (#|V| * #|K|)%N by rewrite -mulVK coprime_cardMg.
have tiVK_P: V <*> K :&: P = 1.
  have sylV: p.-Sylow(V <*> K) V.
    by rewrite /pHall pV -divgS joing_subl //= oVK mulKn.
  apply/trivgP; rewrite -tiVP subsetI subsetIr.
  rewrite (sub_normal_Hall sylV) ?subsetIl ?(pgroupS (subsetIr _ P)) //=.
  by rewrite /normal joing_subl join_subG normG.
have{mulVK oVK} oH: (#|H| = #|V| * #|K| * #|P|)%N.
  by rewrite -defH mulVK -oVK (TI_cardMg tiVK_P).
have{oH tiVK_P IHsub} IHsub: forall X : {group gT},
  P <*> R \subset 'N(X) -> X \subset K -> X :=: K \/ X \subset 'C(P).
- move=> X nX_PR sXK; have p'X: p^'.-group X := pgroupS sXK p'K.
  have nXP: P \subset 'N(X) := subset_trans (joing_subl P R) nX_PR.
  apply/predU1P; rewrite eqEcard sXK; case: leqP => //= ltXK.
  apply/commG1P; rewrite {}IHsub // orbF (norm_joinEr (normsY _ _)) //=.
  rewrite TI_cardMg /=; last first.
    by apply/trivgP; rewrite -tiVK_P setSI ?genS ?setUS.
  rewrite oH ltn_pmul2r ?cardG_gt0 // norm_joinEr ?(subset_trans sXK) //.
  by rewrite coprime_cardMg ?ltn_pmul2l ?(pnat_coprime pV).
have defKP: [~: K, P] = K.
  have sKP_K: [~: K, P] \subset K by rewrite commg_subl.
  have{sKP_K} [|//|cP_KP] := IHsub _ _ sKP_K.
    by rewrite join_subG /= commg_normr normsR.
  by case/eqP: ntKP; rewrite -coprime_commGid ?(commG1P cP_KP) ?(solvableS sKH).
have nKPR: P <*> R \subset 'N(K) by rewrite join_subG nKP.
have coPR: coprime #|P| #|R| by rewrite (coprimeSg sPH).
have{scKH} tiPRcK: 'C_(P <*> R)(K) = 1.
  have tiPK: P :&: K = 1 by rewrite setIC coprime_TIg.
  have tiPcK: 'C_P(K) = 1.
    by apply/trivgP; rewrite /= -{1}(setIidPl sPH) -setIA -tiPK setIS.
  have tiRcK: 'C_R(K) = 1.
    by rewrite prime_TIg ?oR // centsC (sameP commG1P eqP).
  have mulPR: P * R = P <*> R by rewrite norm_joinEr.
  by rewrite -(coprime_mulG_setI_norm mulPR) ?tiPcK ?mul1g ?norms_cent.
have [K1 | ntK]:= eqsVneq K 1; first by rewrite K1 comm1G eqxx in ntKR.
have [K1 | [q q_pr q_dv_K]] := trivgVpdiv K; first by case/eqP: ntK.
have q_gt1 := prime_gt1 q_pr.
have p'q: q != p by apply: (pgroupP p'K).
have{r'K} q'r: r != q by rewrite eq_sym; apply: (pgroupP r'K).
have{defK} qK: q.-group K.
  have{defK} nilK: nilpotent K by rewrite -defK Fitting_nil.
  have{nilK} [_ defK _ _] := dprodP (nilpotent_pcoreC q nilK).
  have{IHsub} IHpi: forall pi, 'O_pi(K) = K \/ 'O_pi(K) \subset 'C(P).
    move=> pi; apply: IHsub (pcore_sub _ _).
    by rewrite gFnorm_trans // join_subG nKP.
  case: (IHpi q) => [<-| cPKq]; first exact: pcore_pgroup.
  case/eqP: ntKP; apply/commG1P; rewrite -{}defK mul_subG //.
  case: (IHpi q^') => // defK; case/idPn: q_dv_K.
  by rewrite -p'natE // -defK; apply: pcore_pgroup.
pose K' := K^`(1); have charK': K' \char K := der_char 1 K.
have nsK'K: K' <| K := der_normal 1 K; have [sK'K nK'K] := andP nsK'K.
have nK'PR: P <*> R \subset 'N(K') := char_norm_trans charK' nKPR.
have iK'K: 'C_(P <*> R / K')(K / K') = 1 -> #|K / K'| > q ^ 2.
  have qKb: q.-group (K / K') by apply: morphim_pgroup qK.
  rewrite ltnNge => trCK'; apply: contra ntKP => Kq_le_q2.
  suffices sPR_K': [~: P, R] \subset K'.
    rewrite -defP -(setIidPl sPR_K') coprime_TIg ?commG1 //.
    by rewrite (pnat_coprime (pgroupS _ pP) (pgroupS sK'K p'K)) ?commg_subl.
  rewrite -quotient_cents2 ?(char_norm_trans charK') //.
  suffices cPRbPrb: abelian (P <*> R / K').
    by rewrite (sub_abelian_cent2 cPRbPrb) ?quotientS ?joing_subl ?joing_subr.
  have nKbPR: P <*> R / K' \subset 'N(K / K') by apply: quotient_norms.
  case cycK: (cyclic (K / K')).
    rewrite (isog_abelian (quotient1_isog _)) -trCK' -ker_conj_aut.
    rewrite (isog_abelian (first_isog_loc _ _)) //.
    by rewrite (abelianS (Aut_conj_aut _ _)) ?Aut_cyclic_abelian.
  have{cycK} [oKb abelKb]: #|K / K'| = (q ^ 2)%N /\ q.-abelem (K / K').
    have sKb1: 'Ohm_1(K / K') \subset K / K' by apply: Ohm_sub.
    have cKbKb: abelian (K / K') by rewrite sub_der1_abelian.
    have: #|'Ohm_1(K / K')| >= q ^ 2.
      rewrite (card_pgroup (pgroupS sKb1 qKb)) leq_exp2l // ltnNge.
      by rewrite -p_rank_abelian -?rank_pgroup // -abelian_rank1_cyclic ?cycK.
    rewrite (geq_leqif (leqif_trans (subset_leqif_card sKb1) (leqif_eq _))) //.
    by case/andP=> sKbKb1; move/eqP->; rewrite (abelemS sKbKb1) ?Ohm1_abelem.
  have ntKb: K / K' != 1 by rewrite -cardG_gt1 oKb (ltn_exp2l 0).
  pose rPR := abelem_repr abelKb ntKb nKbPR.
  have: mx_faithful rPR by rewrite abelem_mx_faithful.
  move: rPR; rewrite (dim_abelemE abelKb ntKb) oKb pfactorK // => rPR ffPR.
  apply: charf'_GL2_abelian ffPR _.
    by rewrite quotient_odd ?(oddSg _ oddG) // join_subG (subset_trans sPH).
  rewrite (eq_pgroup _ (eq_negn (charf_eq (char_Fp q_pr)))).
  rewrite quotient_pgroup //= norm_joinEr // pgroupM.
  by rewrite /pgroup (pi_pnat rR) // (pi_pnat pP) // !inE eq_sym.
case cKK: (abelian K); last first.
  have [|[dPhiK dK'] dCKP] := abelian_charsimple_special qK coKP defKP.
    apply/bigcupsP=> L /andP[charL]; have sLK := char_sub charL. 
    by case/IHsub: sLK cKK => // [|-> -> //]; apply: char_norm_trans charL _.
  have eK: exponent K %| q.
    have oddK: odd #|K| := oddSg sKG oddG.
    have [Q [charQ _ _ eQ qCKQ]] := critical_odd qK oddK ntK; rewrite -eQ.
    have sQK: Q \subset K := char_sub charQ.
    have [<- // | cQP] := IHsub Q (char_norm_trans charQ nKPR) sQK.
    case/negP: ntKP; rewrite (sameP eqP commG1P) centsC.
    rewrite -ker_conj_aut -sub_morphim_pre // subG1 trivg_card1.
    rewrite (pnat_1 (morphim_pgroup _ pP) (pi_pnat (pgroupS _ qCKQ) _)) //.
    apply/subsetP=> a; case/morphimP=> x nKx Px ->{a}.
    rewrite /= astab_ract inE /= Aut_aut; apply/astabP=> y Qy.
    rewrite [_ y _]norm_conj_autE ?(subsetP sQK) //.
    by rewrite /conjg (centsP cQP y) ?mulKg.
  have tiPRcKb: 'C_(P <*> R / K')(K / K') = 1.
    rewrite -quotient_astabQ -quotientIG /=; last first.
      by rewrite sub_astabQ normG trivg_quotient sub1G.
    apply/trivgP; rewrite -quotient1 quotientS // -tiPRcK subsetI subsetIl /=.
    rewrite (coprime_cent_Phi qK) ?(coprimegS (subsetIl _ _)) //=.
      by rewrite norm_joinEr // coprime_cardMg // coprime_mulr coKP.
    rewrite dPhiK -dK' -/K' (subset_trans (commgS _ (subsetIr _ _))) //.
    by rewrite astabQ -quotient_cents2 ?subsetIl // cosetpreK centsC /=.
  have [nK'P nK'R] := (char_norm_trans charK' nKP, char_norm_trans charK' nKR).
  have solK: solvable K := pgroup_sol qK.
  have dCKRb: 'C_K(R) / K' = 'C_(K / K')(R / K').
    by rewrite coprime_quotient_cent.
  have abelKb: q.-abelem (K / K') by rewrite [K']dK' -dPhiK Phi_quotient_abelem.
  have [qKb cKbKb _] := and3P abelKb.
  have [tiKcRb | ntCKRb]:= eqVneq 'C_(K / K')(R / K') 1.
    have coK'P: coprime #|K'| #|P| by rewrite (coprimeSg sK'K).
    suffices sPK': P \subset K'.
      by case/negP: ntKP; rewrite -(setIidPr sPK') coprime_TIg ?commG1.
    rewrite -quotient_sub1 // -defP commGC quotientR //= -/K'.
    have <-: 'C_(P / K')(K / K') = 1.
      by apply/trivgP; rewrite -tiPRcKb setSI ?morphimS ?joing_subl.
    have q'P: q^'.-group P by rewrite /pgroup (pi_pnat pP) // !inE eq_sym.
    move: tiKcRb; have: q^'.-group (P <*> R / K').
      rewrite quotient_pgroup //= norm_joinEr //.
      by rewrite pgroupM q'P /pgroup oR pnatE.
    have sPRG: P <*> R \subset G by rewrite join_subG sRG (subset_trans sPH).
    have coPRb: coprime #|P / K'| #|R / K'| by rewrite coprime_morph.
    apply: odd_prime_sdprod_abelem_cent1 abelKb _; rewrite ?quotient_norms //.
    - by rewrite quotient_sol // (solvableS sPRG).
    - by rewrite quotient_odd // (oddSg sPRG).
    - by rewrite /= quotientY // sdprodEY ?quotient_norms ?coprime_TIg.
    rewrite -(card_isog (quotient_isog nK'R _)) ?oR //.
    by rewrite coprime_TIg // (coprimeSg sK'K).
  have{ntCKRb} not_sCKR_K': ~~ ('C_K(R) \subset K').
    by rewrite -quotient_sub1 ?subIset ?nK'K // dCKRb subG1.
  have oCKR: #|'C_K(R)| = q.
    have [x defCKR]: exists x, 'C_K(R) = <[x]>.
      have ZgrCKR: Zgroup 'C_K(R) := ZgroupS (setSI _ sKH) ZgrCHR.
      have qCKR: q.-group 'C_K(R) by rewrite (pgroupS (subsetIl K _)).
      by apply/cyclicP; apply: nil_Zgroup_cyclic (pgroup_nil qCKR).
    have Kx: x \in K by rewrite -cycle_subG -defCKR subsetIl.
    rewrite defCKR cycle_subG in not_sCKR_K' *.
    exact: nt_prime_order (exponentP eK x Kx) (group1_contra not_sCKR_K').
  have tiCKR_K': 'C_K(R) :&: K' = 1 by rewrite prime_TIg ?oCKR.
  have sKR_K: [~: K, R] \subset K by rewrite commg_subl nKR.
  have ziKRcR: 'C_K(R) :&: [~: K, R] \subset K'.
    rewrite -quotient_sub1 ?subIset ?nK'K // setIC.
    rewrite (subset_trans (quotientI _ _ _)) // dCKRb setIA.
    rewrite (setIidPl (quotientS _ sKR_K)) // ?quotientR //= -/K'.
    by rewrite coprime_abel_cent_TI ?quotient_norms ?coprime_morph.
  have not_sK_KR: ~~ (K \subset [~: K, R]).
    by apply: contra not_sCKR_K' => sK_KR; rewrite -{1}(setIidPl sK_KR) setIAC.
  have tiKRcR: 'C_[~: K, R](R) = 1.
    rewrite -(setIidPr sKR_K) setIAC -(setIidPl ziKRcR) setIAC tiCKR_K'.
    by rewrite (setIidPl (sub1G _)).
  have cKR_KR: abelian [~: K, R].
    have: 'C_[~: K, R](V) \subset [1].
      rewrite -tiVN -{2}scVH -setIIr setICA setIC setIS //.
      exact: subset_trans sKR_K sKN.
    rewrite /abelian (sameP commG1P trivgP) /= -derg1; apply: subset_trans.
    have nKR_R: R \subset 'N([~: K, R]) by rewrite commg_normr.
    have sKRR_G: [~: K, R] <*> R \subset G by rewrite join_subG comm_subG.
    move: oCVR; have: p^'.-group ([~: K, R] <*> R).
      by rewrite norm_joinEr // pgroupM (pgroupS sKR_K p'K) /pgroup oR pnatE.
    have solKR_R := solvableS sKRR_G solG.
    apply: Frobenius_prime_cent_prime; rewrite ?oR ?(subset_trans _ nVG) //.
    by rewrite sdprodEY // coprime_TIg // (coprimeSg sKR_K).
  case nKR_P: (P \subset 'N([~: K, R])).
    have{nKR_P} nKR_PR: P <*> R \subset 'N([~: K, R]).
      by rewrite join_subG nKR_P commg_normr.
    have{nKR_PR} [dKR | cP_KR] := IHsub _ nKR_PR sKR_K.
      by rewrite dKR subxx in not_sK_KR.
    have{cP_KR} cKRb: R / K' \subset 'C(K / K').
      by rewrite quotient_cents2r //= dK' -dCKP commGC subsetI sKR_K.
    case/negP: ntKR; rewrite (sameP eqP commG1P) centsC.
    by rewrite (coprime_cent_Phi qK) // dPhiK -dK' commGC -quotient_cents2.
  have{nKR_P} [x Px not_nKRx] := subsetPn (negbT nKR_P).
  have iKR: #|K : [~: K, R]| = q.
    rewrite -divgS // -{1}(coprime_cent_prod nKR) // TI_cardMg ?mulKn //.
    by rewrite setIA (setIidPl sKR_K).
  have sKRx_K: [~: K, R] :^ x \subset K by rewrite -{2}(normsP nKP x Px) conjSg.
  have nKR_K: K \subset 'N([~: K, R]) by apply: commg_norml.
  have mulKR_Krx: [~: K, R] * [~: K, R] :^ x = K.
    have maxKR: maximal [~: K, R] K by rewrite p_index_maximal ?iKR.
    apply: mulg_normal_maximal; rewrite ?(p_maximal_normal qK) //.
    by rewrite inE in not_nKRx.
  have ziKR_KRx: [~: K, R] :&: [~: K, R] :^ x \subset K'.
    rewrite /K' dK' subsetI subIset ?sKR_K // -{3}mulKR_Krx centM centJ.
    by rewrite setISS ?conjSg.
  suffices: q ^ 2 >= #|K / K'| by rewrite leqNgt iK'K.
  rewrite -divg_normal // leq_divLR ?cardSg //.
  rewrite -(@leq_pmul2l (#|[~: K, R]| ^ 2)) ?expn_gt0 ?cardG_gt0 // mulnA.
  rewrite -expnMn -iKR Lagrange // -mulnn -{2}(cardJg _ x) mul_cardG.
  by rewrite mulKR_Krx mulnAC leq_pmul2l ?muln_gt0 ?cardG_gt0 ?subset_leq_card.
have tiKcP: 'C_K(P) = 1 by rewrite -defKP coprime_abel_cent_TI.
have{IHsub} abelK: q.-abelem K.
  have [/abelem_Ohm1P->//|cPK1] := IHsub _ (gFnorm_trans _ nKPR) (Ohm_sub 1 K).
  rewrite -(setIid K) TI_Ohm1 ?eqxx // in ntK.
  by apply/eqP; rewrite -subG1 -tiKcP setIS.
have{K' iK'K charK' nsK'K sK'K nK'K nK'PR} oKq2: q ^ 2 < #|K|.
  have K'1: K' :=: 1 by apply/commG1P.
  rewrite -indexg1 -K'1 -card_quotient ?normal_norm // iK'K // K'1.
  by rewrite -injm_subcent ?coset1_injm ?norms1 //= tiPRcK morphim1.
pose S := [set Vi : {group gT} | 'C_V('C_K(Vi)) == Vi & maximal 'C_K(Vi) K].
have defSV Vi: Vi \in S -> 'C_V('C_K(Vi)) = Vi by rewrite inE; case: eqP.
have maxSK Vi: Vi \in S -> maximal 'C_K(Vi) K by case/setIdP.
have sSV Vi: Vi \in S -> Vi \subset V by move/defSV <-; rewrite subsetIl.
have ntSV Vi: Vi \in S -> Vi :!=: 1.
  move=> Si; apply: contraTneq (maxgroupp (maxSK _ Si)) => ->.
  by rewrite /= cent1T setIT proper_irrefl.
have nSK Vi: Vi \in S -> K \subset 'N(Vi).
  by move/defSV <-; rewrite normsI ?norms_cent // sub_abelian_norm ?subsetIl.
have defV: <<\bigcup_(Vi in S) Vi>> = V.
  apply/eqP; rewrite eqEsubset gen_subG.
  apply/andP; split; first by apply/bigcupsP; apply: sSV.
  rewrite -(coprime_abelian_gen_cent cKK nVK) ?(pnat_coprime pV) // gen_subG.
  apply/bigcupsP=> Kj /= /and3P[cycKbj sKjK nKjK].
  have [xb defKbj] := cyclicP cycKbj.
  have Kxb: xb \in K / Kj by rewrite defKbj cycle_id.
  set Vj := 'C_V(Kj); have [-> | ntVj] := eqsVneq Vj 1; first exact: sub1G.
  have nt_xb: xb != 1.
    apply: contra ntVj; rewrite -cycle_eq1 -defKbj -!subG1 -tiVcK.
    by rewrite quotient_sub1 // => sKKj; rewrite setIS ?centS.
  have maxKj: maximal Kj K.
    rewrite p_index_maximal // -card_quotient // defKbj -orderE.
    by rewrite (abelem_order_p (quotient_abelem Kj abelK) Kxb nt_xb).
  suffices defKj: 'C_K(Vj) = Kj.
    by rewrite sub_gen // (bigcup_max 'C_V(Kj))%G // inE defKj eqxx.
  have{maxKj} [_ maxKj] := maxgroupP maxKj.
  rewrite ['C_K(Vj)]maxKj //; last by rewrite subsetI sKjK centsC subsetIr.
  rewrite properEneq subsetIl andbT (sameP eqP setIidPl) centsC.
  by apply: contra ntVj; rewrite -subG1 -tiVcK subsetI subsetIl.
pose dxp := [fun D : {set {group gT}} => \big[dprod/1]_(Vi in D) Vi].
have{defV} defV: \big[dprod/1]_(Vi in S) Vi = V.
  have [D maxD]: {D | maxset [pred E | group_set (dxp E) & E \subset S] D}.
    by apply: ex_maxset; exists set0; rewrite /= sub0set big_set0 groupP.
  have [gW sDS] := andP (maxsetp maxD); have{maxD} [_ maxD] := maxsetP maxD.
  have{gW} [W /= defW]: {W : {group gT} | dxp D = W} by exists (Group gW).
  have [eqDS | ltDS] := eqVproper sDS.
    by rewrite eqDS in defW; rewrite defW -(bigdprodWY defW).
  have{ltDS} [_ [Vi Si notDi]] := properP ltDS.
  have sWV: W \subset V.
    rewrite -(bigdprodWY defW) gen_subG.
    by apply/bigcupsP=> Vj Dj; rewrite sSV ?(subsetP sDS).
  suffices{maxD sWV defV} tiWcKi: 'C_W('C_K(Vi)) = 1.
    have:= notDi; rewrite -(maxD (Vi |: D)) ?setU11 ?subsetUr //= subUset sDS.
    rewrite sub1set Si big_setU1 //= defW dprodEY ?groupP //.
      by rewrite (sub_abelian_cent2 cVV) // sSV.
    by rewrite -(defSV Vi Si) setIAC (setIidPr sWV).
  apply/trivgP/subsetP=> w /setIP[Ww cKi_w].
  have [v [Vv def_w v_uniq]] := mem_bigdprod defW Ww.
  rewrite def_w big1 ?inE // => Vj Dj; have Sj := subsetP sDS Vj Dj.
  have cKi_vj: v Vj \in 'C('C_K(Vi)).
    apply/centP=> x Ki_x; apply/commgP/conjg_fixP.
    apply: (v_uniq (fun Vk => v Vk ^ x)) => // [Vk Dk|].
      have [[Kx _] Sk]:= (setIP Ki_x, subsetP sDS Vk Dk).
      by rewrite memJ_norm ?Vv // (subsetP (nSK Vk Sk)).
    rewrite -(mulKg x w) -(centP cKi_w) // -conjgE def_w.
    by apply: (big_morph (conjg^~ x)) => [y z|]; rewrite ?conj1g ?conjMg.
  suffices mulKji: 'C_K(Vj) * 'C_K(Vi) = K.
    by apply/set1gP; rewrite -tiVcK -mulKji centM setIA defSV // inE Vv.
  have maxKj := maxSK Vj Sj; have [_ maxKi] := maxgroupP (maxSK Vi Si).
  rewrite (mulg_normal_maximal _ maxKj) -?sub_abelian_normal ?subsetIl //.
  have [eqVji|] := eqVneq Vj Vi; first by rewrite -eqVji Dj in notDi.
  apply: contra => /= sKiKj; rewrite -val_eqE /= -(defSV Vj Sj).
  by rewrite (maxKi _ (maxgroupp maxKj) sKiKj) defSV.
have nVPR: P <*> R \subset 'N(V) by rewrite join_subG nVP.
have actsPR: [acts P <*> R, on S | 'JG].
  apply/subsetP=> x PRx; rewrite !inE; apply/subsetP=> Vi.
  rewrite !inE /= => Si; rewrite -(normsP nKPR x PRx) !centJ -!conjIg centJ .
  by rewrite -(normsP nVPR x PRx) -conjIg (inj_eq (@conjsg_inj _ _)) maximalJ.
have transPR: [transitive P <*> R, on S | 'JG].
  pose ndxp D (U A B : {group gT}) := dxp (S :&: D) = U -> A * B \subset 'N(U).
  have nV_VK D U: ndxp D U V K.
    move/bigdprodWY <-; rewrite norms_gen ?norms_bigcup //.
    apply/bigcapsP=> Vi /setIP[Si _].
    by rewrite mulG_subG nSK // sub_abelian_norm // sSV.
  have nV_PR D U: [acts P <*> R, on S :&: D | 'JG] -> ndxp D U P R.
    move=> actsU /bigdprodWY<-; rewrite -norm_joinEr ?norms_gen //.
    apply/subsetP=> x PRx; rewrite inE sub_conjg; apply/bigcupsP=> Vi Di.
    by rewrite -sub_conjg (bigcup_max (Vi :^ x)%G) //= (acts_act actsU).
  have [S0 | [V1 S1]] := set_0Vmem S.
    by case/eqP: ntV; rewrite -defV S0 big_set0.
  apply/imsetP; exists V1 => //; set D := orbit _ _ _.
  rewrite (big_setID D) /= setDE in defV.
  have [[U W defU defW] _ _ tiUW] := dprodP defV.
  rewrite defU defW in defV tiUW.
  have [|U1|eqUV]:= indecomposableV _ _ defV.
  - rewrite -mulHR -defH -mulgA mul_subG //.
      by rewrite subsetI (nV_VK _ _ defU) (nV_VK _ _ defW).
    rewrite subsetI (nV_PR _ _ _ defU) ?actsI ?acts_orbit ?subsetT //=.
    by rewrite (nV_PR _ _ _ defW) // actsI ?astabsC ?acts_orbit ?subsetT /=.
  - case/negP: (ntSV V1 S1); rewrite -subG1 -U1 -(bigdprodWY defU) sub_gen //.
    by rewrite (bigcup_max V1) // inE S1 orbit_refl.
  apply/eqP; rewrite eqEsubset (acts_sub_orbit _ actsPR) S1 andbT.
  apply/subsetP=> Vi Si; apply: contraR (ntSV Vi Si) => D'i; rewrite -subG1.
  rewrite -tiUW eqUV subsetI sSV // -(bigdprodWY defW).
  by rewrite (bigD1 Vi) ?joing_subl // inE Si inE.
have [cSR | not_cSR] := boolP (R \subset 'C(S | 'JG)).
  have{cSR} sRnSV: R \subset \bigcap_(Vi in S) 'N(Vi).
    apply/bigcapsP=> Vi Si.
    by rewrite -astab1JG (subset_trans cSR) ?astabS ?sub1set.
  have sPRnSV: P <*> R \subset 'N(\bigcap_(Vi in S) 'N(Vi)).
    apply/subsetP=> x PRx; rewrite inE; apply/bigcapsP=> Vi Si.
    by rewrite sub_conjg -normJ bigcap_inf ?(acts_act actsPR) ?groupV.
  have [V1 S1] := imsetP transPR.
  have: P <*> R \subset 'N(V1).
    rewrite join_subG (subset_trans sRnSV) /= ?bigcap_inf // andbT -defP.
    apply: (subset_trans (commgS P sRnSV)).
    have:= subset_trans (joing_subl P R) sPRnSV; rewrite -commg_subr /=.
    by move/subset_trans; apply; apply: bigcap_inf.
  rewrite -afixJG; move/orbit1P => -> allV1.
  have defV1: V1 = V by apply: group_inj; rewrite /= -defV allV1 big_set1.
  case/idPn: oKq2; rewrite -(Lagrange (subsetIl K 'C(V1))).
  rewrite (p_maximal_index qK (maxSK V1 S1)) defV1 /= tiKcV cards1 mul1n.
  by rewrite (ltn_exp2l 2 1).
have actsR: [acts R, on S | 'JG] := subset_trans (joing_subr P R) actsPR.
have ntSRcR Vi:
    Vi \in S -> ~~ (R \subset 'N(Vi)) ->
  #|Vi| = p /\ 'C_V(R) \subset <<class_support Vi R>>.
- move=> Si not_nViR; have [sVi nV] := (subsetP (sSV Vi Si), subsetP nVR).
  pose f v := fmval (\sum_(x in R) fmod cVV v ^@ x).
  have fM: {in Vi &, {morph f: u v / u * v}}.
    move=> u v /sVi Vu /sVi Vv; rewrite -fmvalA -big_split.
    by congr (fmval _); apply: eq_bigr => x Rx; rewrite /= -actAr fmodM.
  have injf: 'injm (Morphism fM).
    apply/subsetP=> v /morphpreP[Vi_v]; have Vv := sVi v Vi_v.
    rewrite (bigD1 Vi) //= in defV; have [[_ W _ dW] _ _ _] := dprodP defV.
    have [u [w [_ _ uw Uuw]]] := mem_dprod defV (group1 V).
    case: (Uuw 1 1) => // [||u1 w1]; rewrite ?dW ?mulg1 // !inE eq_sym /f /=.
    move/eqP; rewrite (big_setD1 1) // actr1 ?fmodK // fmvalA //= fmval_sum.
    do [case/Uuw; rewrite ?dW ?fmodK -?u1 ?group_prod //] => [x R'x | ->] //.
    rewrite (nt_gen_prime _ R'x) ?cycle_subG ?oR // inE in not_nViR nVR actsR.
    rewrite fmvalJ ?fmodK // -(bigdprodWY dW) ?mem_gen //; apply/bigcupP.
    exists (Vi :^ x)%G; rewrite ?memJ_conjg // (astabs_act _ actsR) Si.
    by apply: contraNneq not_nViR => /congr_group->.
  have im_f: Morphism fM @* Vi \subset 'C_V(R).
    apply/subsetP=> _ /morphimP[v _ Vi_v ->]; rewrite inE fmodP.
    apply/centP=> x Rx; red; rewrite conjgC -fmvalJ ?nV //; congr (x * fmval _).
    rewrite {2}(reindex_acts 'R _ Rx) ?astabsR //= actr_sum.
    by apply: eq_bigr => y Ry; rewrite actrM ?nV.
  have defCVR: Morphism fM @* Vi = 'C_V(R).
    apply/eqP; rewrite eqEcard im_f (prime_nt_dvdP _ _ (cardSg im_f)) ?oCVR //=.
    by rewrite -trivg_card1 morphim_injm_eq1 ?ntSV.
  rewrite -oCVR -defCVR; split; first by rewrite card_injm.
  apply/subsetP=> _ /morphimP[v _ Vi_v ->] /=; rewrite /f fmval_sum.
  have Vv := sVi v Vi_v; apply: group_prod => x Rx.
  by rewrite fmvalJ ?fmodK ?nV // mem_gen // mem_imset2.
have{not_cSR} [V1 S1 not_nV1R]: exists2 V1, V1 \in S & ~~ (R \subset 'N(V1)).
  by move: not_cSR; rewrite astabC; case/subsetPn=> v; rewrite afixJG; exists v.
set D := orbit 'JG%act R V1.
have oD: #|D| = r by rewrite card_orbit astab1JG prime_TIg ?indexg1 ?oR.
have oSV Vi: Vi \in S -> #|Vi| = p.
  move=> Si; have [z _ ->]:= atransP2 transPR S1 Si.
  by rewrite cardJg; case/ntSRcR: not_nV1R.
have cSnS' Vi: Vi \in S -> 'N(Vi)^`(1) \subset 'C(Vi).
  move=> Si; rewrite der1_min ?cent_norm //= -ker_conj_aut.
  rewrite (isog_abelian (first_isog _)) (abelianS (Aut_conj_aut _ _)) //.
  by rewrite Aut_cyclic_abelian // prime_cyclic // oSV.
have nVjR Vj: Vj \in S :\: D -> 'C_K(Vj) = [~: K, R].
  case/setDP=> Sj notDj; set Kj := 'C_K(Vj).
  have [nVjR|] := boolP (R \subset 'N(Vj)).
    have{nVjR} sKRVj: [~: K, R] \subset Kj.
      rewrite subsetI {1}commGC commg_subr nKR.
      by rewrite (subset_trans _ (cSnS' Vj Sj)) // commgSS ?nSK.
    have iKj: #|K : Kj| = q by rewrite (p_maximal_index qK (maxSK Vj Sj)).
    have dxKR: [~: K, R] \x 'C_K(R) = K by rewrite coprime_abelian_cent_dprod.
    have{dxKR} [_ defKR _ tiKRcR] := dprodP dxKR.
    have Z_CK: Zgroup 'C_K(R) by apply: ZgroupS ZgrCHR; apply: setSI.
    have abelCKR: q.-abelem 'C_K(R) := abelemS (subsetIl _ _) abelK.
    have [qCKR _] := andP abelCKR.
    apply/eqP; rewrite eq_sym eqEcard sKRVj -(leq_pmul2r (ltnW q_gt1)).
    rewrite -{1}iKj Lagrange ?subsetIl // -{1}defKR (TI_cardMg tiKRcR).
    rewrite leq_pmul2l ?cardG_gt0 //= (card_pgroup qCKR).
    rewrite (leq_exp2l _ 1) // -abelem_cyclic // (forall_inP Z_CK) //.
    by rewrite (@p_Sylow _ q) // /pHall subxx indexgg qCKR.
  case/ntSRcR=> // _ sCVj; case/ntSRcR: not_nV1R => // _ sCV1.
  suffices trCVR: 'C_V(R) = 1 by rewrite -oCVR trCVR cards1 in p_pr.
  apply/trivgP; rewrite (big_setID D) in defV.
  have{defV} [[W U /= defW defU] _ _ <-] := dprodP defV.
  rewrite defW defU subsetI (subset_trans sCV1) /=; last first.
    rewrite class_supportEr -(bigdprodWY defW) genS //.
    apply/bigcupsP=> x Rx; rewrite (bigcup_max (V1 :^ x)%G) // inE.
    by rewrite (actsP actsR) //= S1 mem_imset.
  rewrite (subset_trans sCVj) // class_supportEr -(bigdprodWY defU) genS //.
  apply/bigcupsP=> x Rx; rewrite (bigcup_max (Vj :^ x)%G) // inE.
  by rewrite (actsP actsR) // Sj andbT (orbit_transl _ (mem_orbit 'JG Vj Rx)).
have sDS: D \subset S.
  by rewrite acts_sub_orbit //; apply: subset_trans actsPR; apply: joing_subr.
have [eqDS | ltDS] := eqVproper sDS.
  have [fix0 | [Vj cVjP]] := set_0Vmem 'Fix_(S | 'JG)(P).
    case/negP: p'r; rewrite eq_sym -dvdn_prime2 // -oD eqDS /dvdn.
    rewrite (pgroup_fix_mod pP (subset_trans (joing_subl P R) actsPR)).
    by rewrite fix0 cards0 mod0n.
  have{cVjP} [Sj nVjP] := setIP cVjP; rewrite afixJG in nVjP.
  case/negP: (ntSV Vj Sj); rewrite -subG1 -tiVcK subsetI sSV // centsC -defKP.
  by rewrite (subset_trans _ (cSnS' Vj Sj)) // commgSS ?nSK.
have [_ [Vj Sj notDj]] := properP ltDS.
have defS: S = Vj |: D.
  apply/eqP; rewrite eqEsubset andbC subUset sub1set Sj sDS.
  apply/subsetP=> Vi Si; rewrite !inE orbC /= -val_eqE /= -(defSV Vi Si).
  have [//|notDi] := boolP (Vi \in _); rewrite -(defSV Vj Sj) /=.
  by rewrite !nVjR // inE ?notDi ?notDj.
suffices: odd #|S| by rewrite defS cardsU1 (negPf notDj) /= oD -oR (oddSg sRG).
rewrite (dvdn_odd (atrans_dvd transPR)) // (oddSg _ oddG) //.
by rewrite join_subG (subset_trans sPH).
Qed.

End Theorem_3_6.

(* This is B & G, Theorem 3.7. *)
Theorem prime_Frobenius_sol_kernel_nil gT (G K R : {group gT}) :
   K ><| R = G -> solvable G -> prime #|R| -> 'C_K(R) = 1 -> nilpotent K.
Proof.
move=> defG solG R_pr regR.
elim: {K}_.+1 {-2}K (ltnSn #|K|) => // m IHm K leKm in G defG solG regR *.
have [nsKG sRG defKR nKR tiKR] := sdprod_context defG.
have [sKG nKG] := andP nsKG.
wlog ntK: / K :!=: 1 by case: eqP => [-> _ | _ ->] //; apply: nilpotent1.
have [L maxL _]: {L : {group gT} | maxnormal L K G & [1] \subset L}.
  by apply: maxgroup_exists; rewrite proper1G ntK norms1.
have [ltLK nLG]:= andP (maxgroupp maxL); have [sLK not_sKL]:= andP ltLK.
have{m leKm IHm}nilL: nilpotent L.
  pose G1 := L <*> R; have nLR := subset_trans sRG nLG.
  have sG1G: G1 \subset G by rewrite join_subG (subset_trans sLK).
  have defG1: L ><| R = G1.
    by rewrite sdprodEY //; apply/eqP; rewrite -subG1 -tiKR setSI.
  apply: (IHm _ _ _ defG1); rewrite ?(solvableS sG1G) ?(oddSg sG1G) //.
    exact: leq_trans (proper_card ltLK) _.
  by apply/eqP; rewrite -subG1 -regR setSI.
have sLG := subset_trans sLK sKG; have nsLG: L <| G by apply/andP.
have sLF: L \subset 'F(G) by apply: Fitting_max.
have frobG: [Frobenius G = K ><| R] by apply/prime_FrobeniusP.
have solK := solvableS sKG solG.
have frobGq := Frobenius_quotient frobG solK nsLG not_sKL.
suffices sKF: K \subset 'F(K) by apply: nilpotentS sKF (Fitting_nil K).
apply: subset_trans (chief_stab_sub_Fitting solG nsKG).
rewrite subsetI subxx; apply/bigcapsP=> [[X Y] /= /andP[chiefXY sXF]].
set V := X / Y; have [maxY nsXG] := andP chiefXY.
have [ltYX nYG] := andP (maxgroupp maxY); have [sYX _]:= andP ltYX.
have [sXG nXG] := andP nsXG; have sXK := subset_trans sXF (Fitting_sub K).
have minV := chief_factor_minnormal chiefXY.
have cVL: L \subset 'C(V | 'Q).
  apply: subset_trans (subset_trans sLF (Fitting_stab_chief solG _)) _ => //.
  exact: (bigcap_inf (X, Y)).
have nVG: {acts G, on group V | 'Q}.
  by split; rewrite ?quotientS ?subsetT // actsQ // normal_norm.
pose V1 := sdpair1 <[nVG]> @* V.
have [p p_pr abelV]: exists2 p, prime p & p.-abelem V.
  apply/is_abelemP; apply: charsimple_solvable (quotient_sol _ _).
    exact: minnormal_charsimple minV.
  exact: nilpotent_sol (nilpotentS sXF (Fitting_nil _)).
have abelV1: p.-abelem V1 by rewrite morphim_abelem.
have injV1 := injm_sdpair1 <[nVG]>.
have ntV1: V1 :!=: 1.
  by rewrite -cardG_gt1 card_injm // cardG_gt1; case/andP: (mingroupp minV).
have nV1_G1 := im_sdpair_norm <[nVG]>.
pose rV := morphim_repr (abelem_repr abelV1 ntV1 nV1_G1) (subxx G).
have def_kerV: rker rV = 'C_G(V | 'Q).
  rewrite rker_morphim rker_abelem morphpreIdom morphpreIim -astabEsd //.
  by rewrite astab_actby setIid.
have kerL: L \subset rker rV by rewrite def_kerV subsetI sLG.
pose rVq := quo_repr kerL nLG.
suffices: K / L \subset rker rVq.
  rewrite rker_quo def_kerV quotientSGK //= 1?subsetI 1?(subset_trans sKG) //.
  by rewrite sLG.
have irrVq: mx_irreducible rVq.
  apply/quo_mx_irr; apply/morphim_mx_irr; apply/abelem_mx_irrP.
  apply/mingroupP; rewrite ntV1; split=> // U1; case/andP=> ntU1 nU1G sU1V.
  rewrite -(morphpreK sU1V); congr (_ @* _).
  case/mingroupP: minV => _; apply; last by rewrite sub_morphpre_injm.
  rewrite -subG1 sub_morphpre_injm ?sub1G // morphim1 subG1 ntU1 /=.
  set U := _ @*^-1 U1; rewrite -(cosetpreK U) quotient_norms //.
  have: [acts G, on U | <[nVG]>] by rewrite actsEsd ?subsetIl // morphpreK.
  rewrite astabs_actby subsetI subxx (setIidPr _) ?subsetIl //=.
  by rewrite -{1}(cosetpreK U) astabsQ ?normal_cosetpre //= -/U subsetI nYG.
have [q q_pr abelKq]: exists2 q, prime q & q.-abelem (K / L).
  apply/is_abelemP; apply: charsimple_solvable (quotient_sol _ solK).
  exact: maxnormal_charsimple maxL.
case (eqVneq q p) => [def_q | neq_qp].
  have sKGq: K / L \subset G / L by apply: quotientS.
  rewrite rfix_mx_rstabC //; have [_ _]:= irrVq; apply; rewrite ?submx1 //.
    by rewrite normal_rfix_mx_module ?quotient_normal.
  rewrite -(rfix_subg _ sKGq) (@rfix_pgroup_char _ p) ?char_Fp -?def_q //.
  exact: (abelem_pgroup abelKq).
suffices: rfix_mx rVq (R / L) == 0.
  apply: contraLR; apply: (Frobenius_rfix_compl frobGq).
  apply: pi_pnat (abelem_pgroup abelKq) _.
  by rewrite inE /= (charf_eq (char_Fp p_pr)).
rewrite -mxrank_eq0 (rfix_quo _ _ sRG) (rfix_morphim _ _ sRG).
rewrite (rfix_abelem _ _ _ (morphimS _ sRG)) mxrank_eq0 rowg_mx_eq0 -subG1.
rewrite (sub_abelem_rV_im _ _ _ (subsetIl _ _)) -(morphpreSK _ (subsetIl _ _)).
rewrite morphpreIim -gacentEsd gacent_actby gacentQ (setIidPr sRG) /=.
rewrite -coprime_quotient_cent ?(solvableS sXG) ?(subset_trans sRG) //.
  by rewrite {1}['C_X(R)](trivgP _) ?quotient1 ?sub1G // -regR setSI.
by apply: coprimeSg sXK _; apply: Frobenius_coprime frobG.
Qed.

Corollary Frobenius_sol_kernel_nil gT (G K H : {group gT}) :
  [Frobenius G = K ><| H] -> solvable G -> nilpotent K.
Proof.
move=> frobG solG; have [defG ntK ntH _ _] := Frobenius_context frobG.
have{defG} /sdprodP[_ defG nKH tiKH] := defG.
have[H1 | [p p_pr]] := trivgVpdiv H; first by case/eqP: ntH.
case/Cauchy=> // x Hx ox; rewrite -ox in p_pr.
have nKx: <[x]> \subset 'N(K) by rewrite cycle_subG (subsetP nKH).
have tiKx: K :&: <[x]> = 1 by apply/trivgP; rewrite -tiKH setIS ?cycle_subG.
apply: (prime_Frobenius_sol_kernel_nil (sdprodEY nKx tiKx)) => //.
  by rewrite (solvableS _ solG) // join_subG -mulG_subG -defG mulgS ?cycle_subG.
by rewrite cent_cycle (Frobenius_reg_ker frobG) // !inE -order_gt1 prime_gt1.
Qed.

(* This is B & G, Theorem 3.8. *)
Theorem odd_sdprod_primact_commg_sub_Fitting gT (G K R : {group gT}) :
    K ><| R = G -> odd #|G| -> solvable G ->
  (*1*) coprime #|K| #|R| ->
  (*2*) semiprime K R ->
  (*3*) 'C_('F(K))(R) = 1 ->
  [~: K, R] \subset 'F(K).
Proof.
elim: {G}_.+1 {-2}G (ltnSn #|G|) K R => // n IHn G.
rewrite ltnS => leGn K R defG oddG solG coKR primR regR_F.
have [nsKG sRG defKR nKR tiKR] := sdprod_context defG.
have [sKG nKG] := andP nsKG.
have chF: 'F(K) \char K := Fitting_char K; have nFR := char_norm_trans chF nKR.
have nsFK := char_normal chF; have [sFK nFK] := andP nsFK.
pose KqF := K / 'F(K); have solK := solvableS sKG solG.
without loss [p p_pr pKqF]: / exists2 p, prime p & p.-group KqF.
  move=> IHp;  apply: wlog_neg => IH_KR; rewrite -quotient_cents2 //= -/KqF.
  set Rq := R / 'F(K); have nKRq: Rq \subset 'N(KqF) by apply: quotient_norms.
  rewrite centsC.
  apply: subset_trans (coprime_cent_Fitting nKRq _ _); last first.
  - exact: quotient_sol.
  - exact: coprime_morph.
  rewrite subsetI subxx centsC -['F(KqF)]Sylow_gen gen_subG.
  apply/bigcupsP=> Pq /SylowP[p p_pr /= sylPq]; rewrite -/KqF in sylPq.
  have chPq: Pq \char KqF.
   apply: char_trans (Fitting_char _); rewrite /= -/KqF.
    by rewrite (nilpotent_Hall_pcore (Fitting_nil _) sylPq) ?pcore_char.
  have [P defPq sFP sPK] := inv_quotientS nsFK (char_sub chPq).
  have nsFP: 'F(K) <| P by rewrite /normal sFP (subset_trans sPK).
  have{chPq} chP: P \char K.
    by apply: char_from_quotient nsFP (Fitting_char _) _; rewrite -defPq.
  have defFP: 'F(P) = 'F(K).
    apply/eqP; rewrite eqEsubset !Fitting_max ?Fitting_nil //.
    by rewrite char_normal ?gFchar_trans.
  have coPR := coprimeSg sPK coKR.
  have nPR: R \subset 'N(P) := char_norm_trans chP nKR.
  pose G1 := P <*> R.
  have sG1G: G1 \subset G by rewrite /G1 -defKR norm_joinEr ?mulSg.
  have defG1: P ><| R = G1 by rewrite sdprodEY ?coprime_TIg.
  rewrite defPq quotient_cents2r //= -defFP.
  have:= sPK; rewrite subEproper; case/predU1P=> [defP | ltPK].
    rewrite IHp // in IH_KR; exists p => //.
    by rewrite /KqF -{2}defP -defPq (pHall_pgroup sylPq).
  move/IHn: defG1 => ->; rewrite ?(oddSg sG1G) ?(solvableS sG1G) ?defFP //.
    apply: leq_trans leGn; rewrite /= norm_joinEr //.
    by rewrite -defKR !coprime_cardMg // ltn_pmul2r ?proper_card.
  by move=> x Rx; rewrite -(setIidPl sPK) -!setIA primR.
without loss r_pr: / prime #|R|; last set r := #|R| in r_pr.
  have [-> _ | [r r_pr]] := trivgVpdiv R; first by rewrite commG1 sub1G.
  case/Cauchy=> // x; rewrite -cycle_subG subEproper orderE; set X := <[x]>.
  case/predU1P=> [-> -> -> // | ltXR rX _]; have sXR := proper_sub ltXR.
  have defCX: 'C_K(X) = 'C_K(R).
    rewrite cent_cycle primR // !inE -order_gt1 orderE rX prime_gt1 //=.
    by rewrite -cycle_subG.
  have primX: semiprime K X.
    by move=> y; case/setD1P=> nty Xy; rewrite primR // !inE nty (subsetP sXR).
  have nKX := subset_trans sXR nKR; have coKX := coprimegS sXR coKR.
  pose H := K <*> X; have defH: K ><| X = H by rewrite sdprodEY ?coprime_TIg.
  have sHG: H \subset G by rewrite /H -defKR norm_joinEr ?mulgSS.
  have ltHn: #|H| < n.
    rewrite (leq_trans _ leGn) /H ?norm_joinEr // -defKR !coprime_cardMg //.
    by rewrite ltn_pmul2l ?proper_card.
  have oddH := oddSg sHG oddG; have solH := solvableS sHG solG.
  have regX_F: 'C_('F(K))(X) = 1.
   by rewrite -regR_F -(setIidPl sFK) -!setIA defCX.
  have:= IHn _ ltHn _ _ defH oddH solH coKX primX regX_F.
  rewrite -!quotient_cents2 ?(subset_trans sXR) //; move/setIidPl <-.
  rewrite -coprime_quotient_cent ?(subset_trans sXR) // defCX.
  by rewrite coprime_quotient_cent ?subsetIr.
apply: subset_trans (chief_stab_sub_Fitting solG nsKG) => //.
rewrite subsetI commg_subl nKR; apply/bigcapsP => [[U V]] /=.
case/andP=> chiefUV sUF; set W := U / V.
have minW := chief_factor_minnormal chiefUV.
have [ntW nWG] := andP (mingroupp minW).
have /andP[/maxgroupp/andP[/andP[sVU _] nVG] nsUG] := chiefUV.
have sUK := subset_trans sUF sFK; have sVK := subset_trans sVU sUK.
have nVK := subset_trans sKG nVG; have nVR := subset_trans sRG nVG.
have [q q_pr abelW]: exists2 q, prime q & q.-abelem W.
  apply/is_abelemP; apply: charsimple_solvable (minnormal_charsimple minW) _.
  by rewrite quotient_sol // (solvableS sUK).
have regR_W: 'C_(W)(R / V) = 1.
  rewrite -coprime_quotient_cent ?(coprimeSg sUK) ?(solvableS sUK) //.
  by rewrite -(setIidPl sUF) -setIA regR_F (setIidPr _) ?quotient1 ?sub1G.
rewrite sub_astabQ comm_subG ?quotientR //=.
have defGv: (K / V) * (R / V) = G / V by rewrite -defKR quotientMl.
have oRv: #|R / V| = r.
  rewrite card_quotient // -indexgI -(setIidPr sVK) setICA setIA tiKR.
  by rewrite (setIidPl (sub1G _)) indexg1.
have defCW: 'C_(G / V)(W) = 'C_(K / V)(W).
  apply/eqP; rewrite eqEsubset andbC setSI ?quotientS //=.
  rewrite subsetI subsetIr /= andbT.
  rewrite -(coprime_mulG_setI_norm defGv) ?coprime_morph ?norms_cent //=.
  suffices ->: 'C_(R / V)(W) = 1 by rewrite mulg1 subsetIl.
  apply/trivgP; apply/subsetP=> x; case/setIP=> Rx cWx.
  apply: contraR ntW => ntx; rewrite -subG1 -regR_W subsetI subxx centsC /= -/W.
  by apply: contraR ntx; move/prime_TIg <-; rewrite ?oRv // inE Rx.
have [P sylP nPR] := coprime_Hall_exists p nKR coKR solK.
have [sPK pP _] := and3P sylP.
have nVP := subset_trans sPK nVK; have nFP := subset_trans sPK nFK.
have sylPv: p.-Sylow(K / V) (P / V) by rewrite quotient_pHall.
have defKv: (P / V) * 'C_(G / V)(W) = (K / V).
  rewrite defCW; apply/eqP; rewrite eqEsubset mulG_subG subsetIl quotientS //=.
  have sK_PF: K \subset P * 'F(K).
    rewrite (normC nFP) -quotientSK // subEproper eq_sym eqEcard quotientS //=.
    by rewrite (card_Hall (quotient_pHall nFP sylP)) part_pnat_id ?leqnn.
  rewrite (subset_trans (quotientS _ sK_PF)) // quotientMl // mulgS //.
  rewrite subsetI -quotient_astabQ !quotientS //.
  by rewrite (subset_trans (Fitting_stab_chief solG nsKG)) ?(bigcap_inf (U, V)).
have nW_ := subset_trans (quotientS _ _) nWG; have nWK := nW_ _ sKG. 
rewrite -quotient_cents2 ?norms_cent ?(nW_ _ sRG) //.
have [eq_qp | p'q] := eqVneq q p.
  apply: subset_trans (sub1G _); rewrite -trivg_quotient quotientS // centsC.
  apply/setIidPl; case/mingroupP: minW => _; apply; last exact: subsetIl.
  rewrite andbC normsI ?norms_cent // ?quotient_norms //=.
  have nsWK: W <| K / V by rewrite /normal quotientS.
  have sWP: W \subset P / V.
    by rewrite (normal_sub_max_pgroup (Hall_max sylPv)) -?eq_qp ?abelem_pgroup.
  rewrite -defKv centM setIA setIAC /=.
  rewrite ['C_W(_)](setIidPl _); last by rewrite centsC subsetIr.
  have nilPv: nilpotent (P / V) := pgroup_nil (pHall_pgroup sylPv).
  rewrite -/W -(setIidPl sWP) -setIA meet_center_nil //.
  exact: normalS (quotientS V sPK) nsWK.
rewrite -defKv -quotientMidr -mulgA mulSGid ?subsetIr // quotientMidr.
have sPG := subset_trans sPK sKG.
rewrite quotient_cents2 ?norms_cent ?nW_ //= commGC.
pose Hv := (P / V) <*> (R / V).
have sHGv: Hv \subset G / V by rewrite join_subG !quotientS.
have solHv: solvable Hv := solvableS sHGv (quotient_sol V solG).
have sPHv: P / V \subset Hv by apply: joing_subl.
have nPRv: R / V \subset 'N(P / V) := quotient_norms _ nPR.
have coPRv: coprime #|P / V| #|R / V| := coprime_morph _ (coprimeSg sPK coKR).
apply: subset_trans (subsetIr (P / V) _).
have oHv: #|Hv| = (#|P / V| * #|R / V|)%N.
  by rewrite /Hv norm_joinEr // coprime_cardMg // oRv.
move/(odd_prime_sdprod_abelem_cent1 solHv): (abelW); apply=> //.
- exact: oddSg sHGv (quotient_odd _ _).
- by rewrite sdprodEY ?quotient_norms // coprime_TIg.
- by rewrite oRv.
- by rewrite (subset_trans _ nWG) ?join_subG ?quotientS.
rewrite /= norm_joinEr // pgroupM /pgroup.
rewrite (pi_pnat (quotient_pgroup _ pP)) ?inE 1?eq_sym //=.
apply: coprime_p'group (abelem_pgroup abelW) ntW.
by rewrite coprime_sym coprime_morph // (coprimeSg sUK).
Qed.

(* This is B & G, Proposition 3.9 (for external action), with the incorrectly *)
(* omitted nontriviality assumption reinstated.                               *)
Proposition ext_odd_regular_pgroup_cyclic (aT rT : finGroupType) p
              (D R : {group aT}) (K H : {group rT}) (to : groupAction D K) :
    p.-group R -> odd #|R| -> H :!=: 1 ->
    {acts R, on group H | to} -> {in R^#, forall x, 'C_(H | to)[x] = 1} ->
  cyclic R.
Proof.
move: R H => R0 H0 pR0 oddR0 ntH0 actsR0 regR0.
pose gT := sdprod_groupType <[actsR0]>.
pose H : {group gT} := (sdpair1 <[actsR0]> @* H0)%G.
pose R : {group gT} := (sdpair2 <[actsR0]> @* R0)%G.
pose G : {group gT} := [set: gT]%G.
have{pR0} pR: p.-group R by rewrite morphim_pgroup.
have{oddR0} oddR: odd #|R| by rewrite morphim_odd.
have [R1 | ntR] := eqsVneq R 1.
  by rewrite -(im_invm (injm_sdpair2 <[actsR0]>)) {2}R1 morphim1 cyclic1.
have{ntH0} ntH: H :!=: 1.
  apply: contraNneq ntH0 => H1.
  by rewrite -(im_invm (injm_sdpair1 <[actsR0]>)) {2}H1 morphim1.
have{regR0 ntR} frobG: [Frobenius G = H ><| R].
  apply/Frobenius_semiregularP => // [|x]; first exact: sdprod_sdpair.
  case/setD1P=> nt_x; case/morphimP=> x2 _ Rx2 def_x.
  apply/trivgP; rewrite -(morphpreSK _ (subsetIl _ _)) morphpreI.
  rewrite /= -cent_cycle def_x -morphim_cycle // -gacentEsd.
  rewrite injmK ?injm_sdpair1 // (trivgP (injm_sdpair1 _)).
  rewrite -(regR0 x2) ?inE ?Rx2 ?andbT; last first.
    by apply: contra nt_x; rewrite def_x; move/eqP->; rewrite morph1.
  have [sRD sHK]: R0 \subset D /\ H0 \subset K by case actsR0; move/acts_dom.
  have sx2R: <[x2]> \subset R0 by rewrite cycle_subG.
  rewrite gacent_actby setIA setIid (setIidPr sx2R).
  rewrite !gacentE ?cycle_subG ?sub1set ?(subsetP sRD) //.
  by rewrite !setIS ?afixS ?sub_gen.
suffices: cyclic R by rewrite (injm_cyclic (injm_sdpair2 _)).
move: gT H R G => {aT rT to D K H0 R0 actsR0} gT H R G in ntH pR oddR frobG *.
have [defG _ _ _ _] := Frobenius_context frobG; case/sdprodP: defG => _ _ nHR _.
have coHR := Frobenius_coprime frobG.
rewrite (odd_pgroup_rank1_cyclic pR oddR) leqNgt.
apply: contra ntH => /p_rank_geP[E /pnElemP[sER abelE dimE2]].
have ncycE: ~~ cyclic E by rewrite (abelem_cyclic abelE) dimE2.
have nHE := subset_trans sER nHR; have coHE := coprimegS sER coHR.
rewrite -subG1 -(coprime_abelian_gen_cent1 _ _ nHE) ?(abelem_abelian abelE) //.
rewrite -bigprodGE big1 // => x /setD1P[nt_x Ex]; apply: val_inj => /=.
by apply: (Frobenius_reg_ker frobG); rewrite !inE nt_x (subsetP sER).
Qed.

(* Internal action version of B & G, Proposition 3.9 (possibly, the only one  *)
(* we should keep). *)
Proposition odd_regular_pgroup_cyclic gT p (H R : {group gT}) :
    p.-group R -> odd #|R| -> H :!=: 1 -> R \subset 'N(H) -> semiregular H R ->
  cyclic R.
Proof.
move=> pR oddR ntH nHR regR.
have actsR: {acts R, on group H | 'J} by split; rewrite ?subsetT ?astabsJ.
apply: ext_odd_regular_pgroup_cyclic pR oddR ntH actsR _ => // x Rx.
by rewrite gacentJ cent_set1 regR.
Qed.

(* Another proof of Proposition 3.9, which avoids Frobenius groups entirely.  *)
Proposition simple_odd_regular_pgroup_cyclic gT p (H R : {group gT}) :
    p.-group R -> odd #|R| -> H :!=: 1 -> R \subset 'N(H) -> semiregular H R ->
  cyclic R.
Proof.
move=> pR oddR ntH nHR regR; rewrite (odd_pgroup_rank1_cyclic pR oddR) leqNgt.
apply: contra ntH => /p_rank_geP[E /pnElemP[sER abelE dimE2]].
have ncycE: ~~ cyclic E by rewrite (abelem_cyclic abelE) dimE2.
have nHE := subset_trans sER nHR.
have coHE := coprimegS sER (regular_norm_coprime nHR regR).
rewrite -subG1 -(coprime_abelian_gen_cent1 _ _ nHE) ?(abelem_abelian abelE) //.
rewrite -bigprodGE big1 // => x; case/setD1P=> nt_x Ex; apply: val_inj => /=.
by rewrite regR // !inE nt_x (subsetP sER).
Qed.

(* This is Aschbacher (40.6)(4). *)
Lemma odd_regular_metacyclic gT (H R : {group gT}) :
    odd #|R| -> H :!=: 1 -> R \subset 'N(H) -> semiregular H R ->
  metacyclic R.
Proof.
move=> oddR ntH nHR regHR.
apply/Zgroup_metacyclic/forall_inP=> P /SylowP[p pr_p /and3P[sPR pP _]].
have [oddP nHP] := (oddSg sPR oddR, subset_trans sPR nHR).
exact: odd_regular_pgroup_cyclic pP oddP ntH nHP (semiregularS _ sPR regHR).
Qed.

(* This is Huppert, Kapitel V, Satz 18.8 b (used in Peterfalvi, Section 13). *)
Lemma prime_odd_regular_normal gT (H R P : {group gT}) :
    prime #|P| -> odd #|R| -> P \subset R ->
    H :!=: 1 -> R \subset 'N(H) -> semiregular H R ->
  P <| R.
Proof.
set p := #|P| => pr_p oddR sPR ntH nHR regHR.
have pP: p.-group P := pnat_id pr_p.
have cycQ (q : nat) (Q : {group gT}) : q.-group Q -> Q \subset R -> cyclic Q.
  move=> qQ sQR; have [oddQ nHQ] := (oddSg sQR oddR, subset_trans sQR nHR).
  exact: odd_regular_pgroup_cyclic qQ oddQ ntH nHQ (semiregularS _ sQR regHR).
have cycRq (q : nat): cyclic 'O_q(R) by rewrite (cycQ q) ?pcore_pgroup ?gFsub.
suffices cFP: P \subset 'C('F(R)).
  have nilF: nilpotent 'F(R) := Fitting_nil R.
  have hallRp: p.-Hall('F(R)) 'O_p('F(R)) := nilpotent_pcore_Hall p nilF.
  apply: char_normal_trans (pcore_normal p R); rewrite sub_cyclic_char //=.
  rewrite -p_core_Fitting (sub_normal_Hall hallRp) ?gFnormal //.
  have solR: solvable R.
    by apply: metacyclic_sol; apply: odd_regular_metacyclic regHR.
  by apply: subset_trans (cent_sub_Fitting solR); rewrite subsetI sPR.
rewrite centsC -(bigdprodWY (erefl 'F(R))) gen_subG big_tnth.
apply/bigcupsP=> i _; move: {i}(tuple.tnth _ i) => q.
have [<- | q'p] := eqVneq p q.
  have [Q sylQ sPQ] := Sylow_superset sPR pP; have [sQR pQ _] := and3P sylQ.
  rewrite (sub_abelian_cent2 (cyclic_abelian (cycQ _ _ pQ sQR))) //.
  by rewrite pcore_sub_Hall.
have [-> | ntRq] := eqVneq 'O_q(R) 1%g; first exact: sub1G.
have /andP[sRqR qRq]: q.-subgroup(R) 'O_q(R) by apply: pcore_psubgroup.
have [pr_q _ _] := pgroup_pdiv qRq ntRq.
have coRqP: coprime #|'O_q(R)| p by rewrite (pnat_coprime qRq) // pnatE.
have nRqP: P \subset 'N('O_q(R)) by rewrite (subset_trans sPR) ?gFnorm.
rewrite centsC (coprime_odd_faithful_Ohm1 qRq) ?(oddSg sRqR) //.
apply: sub_abelian_cent2 (joing_subl _ _) (joing_subr _ _) => /=.
set PQ := P <*> _; have oPQ: #|PQ| = (p * q)%N.
  rewrite /PQ norm_joinEl 1?gFnorm_trans //.
  rewrite coprime_cardMg 1?coprime_sym ?(coprimeSg (Ohm_sub 1 _)) // -/p.
  by congr (p * _)%N; apply: Ohm1_cyclic_pgroup_prime => /=.
have sPQ_R: PQ \subset R by rewrite join_subG sPR (subset_trans (Ohm_sub 1 _)).
have nH_PQ := subset_trans sPQ_R nHR.
apply: cyclic_abelian; apply: regular_pq_group_cyclic oPQ ntH nH_PQ _ => //.
exact: semiregularS regHR.
Qed.

Section Wielandt_Frobenius.

Variables (gT : finGroupType) (G K R : {group gT}).
Implicit Type A : {group gT}.

(* This is Peterfalvi (9.1). *)
Lemma Frobenius_Wielandt_fixpoint (M : {group gT}) :
    [Frobenius G = K ><| R] ->
    G \subset 'N(M) -> coprime #|M| #|G| -> solvable M ->
 [/\ (#|'C_M(G)| ^ #|R| * #|M| = #|'C_M(R)| ^ #|R| * #|'C_M(K)|)%N,
     'C_M(R) = 1 -> K \subset 'C(M)
   & 'C_M(K) = 1 -> (#|M| = #|'C_M(R)| ^ #|R|)%N].
Proof.
move=> frobG nMG coMG solM; have [defG _ ntR _ _] := Frobenius_context frobG.
have [_ _ _ _ /eqP snRG] := and5P frobG.
have [nsKG sRG _ _ tiKR] := sdprod_context defG; have [sKG _] := andP nsKG.
pose m0 (_ : {group gT}) := 0%N.
pose Dm := [set 1%G; G]; pose Dn := K |: orbit 'JG K R.
pose m := [fun A => 0%N with 1%G |-> #|K|, G |-> 1%N].
pose n A : nat := A \in Dn.
have out_m: {in [predC Dm], m =1 m0}.
  by move=> A; rewrite !inE /=; case/norP; do 2!move/negbTE->.
have out_n: {in [predC Dn], n =1 m0}.
  by rewrite /n => A /=; move/negbTE=> /= ->.
have ntG: G != 1%G by case: eqP sRG => // -> <-; rewrite subG1.
have neqKR: K \notin orbit 'JG K R.
  apply/imsetP=> [[x _ defK]]; have:= Frobenius_dvd_ker1 frobG.
  by rewrite defK cardJg gtnNdvd // ?prednK // -subn1 subn_gt0 cardG_gt1.
have Gmn A: m A + n A > 0 -> A \subset G.
  rewrite /=; case: eqP => [-> | ] _; first by rewrite sub1G.
  rewrite /n 2!inE; do 2!case: eqP => [-> // | ] _.
  case R_A: (A \in _) => // _; case/imsetP: R_A => x Kx ->{A}.
  by rewrite conj_subG ?(subsetP sKG).
have partG: {in G, forall a,
  \sum_(A | a \in gval A) m A = \sum_(A | a \in gval A) n A}%N.
- move=> a Ga; have [-> | nt_a] := eqVneq a 1.
    rewrite (bigD1 1%G) ?inE ?eqxx //= (bigD1 G) ?inE ?group1 //=.
    rewrite (negbTE ntG) !eqxx big1 ?addn1 => [|A]; last first.
      by rewrite group1 -negb_or -in_set2; apply: out_m.
    rewrite (bigID (mem Dn)) /= addnC big1 => [|A]; last first.
      by rewrite group1; apply: out_n.
    transitivity #|Dn|.
      rewrite cardsU1 neqKR card_orbit astab1JG.
      by rewrite -{3}(setIidPl sKG) -setIA -normD1 snRG tiKR indexg1.
    by rewrite -sum1_card /n; apply: eq_big => [A | A ->]; rewrite ?group1.
  rewrite (bigD1 G) //= (negbTE ntG) eqxx big1 => [|A]; last first.
    case/andP=> Aa neAG; apply: out_m; rewrite !inE; case: eqP => // A1.
    by rewrite A1 inE (negbTE nt_a) in Aa.
  have [partG tiG _] := and3P (Frobenius_partition frobG).
  do [rewrite -(eqP partG); set pG := _ |: _] in Ga tiG.
  rewrite (bigD1 <<pblock pG a>>%G) /=; last by rewrite mem_gen // mem_pblock.
  rewrite big1 => [|B]; last first.
    case/andP=> Ba neqBA; rewrite -/(false : nat); congr (nat_of_bool _).
    apply: contraTF neqBA; rewrite negbK -val_eqE /=.
    case/setU1P=> [BK | /imsetP[x Kx defB]].
      by rewrite (def_pblock tiG _ Ba) BK ?setU11 ?genGid.
    have Rxa: a \in R^# :^ x by rewrite conjD1g !inE nt_a -(congr_group defB).
    rewrite (def_pblock tiG _ Rxa) ?setU1r ?mem_imset // conjD1g.
    by rewrite genD1 ?group1 // genGid defB.
  rewrite /n !inE -val_eqE /= -/(true : nat); congr ((_ : bool) + _)%N.
  case/setU1P: (pblock_mem Ga) => [-> |]; first by rewrite genGid eqxx.
  case/imsetP=> x Kx ->; symmetry; apply/orP; right.
  apply/imsetP; exists x => //.
  by apply: val_inj; rewrite conjD1g /= genD1 ?group1 // genGid.
move/eqP: (solvable_Wielandt_fixpoint Gmn nMG coMG solM partG).
rewrite (bigD1 1%G) // (bigD1 G) //= eqxx (setIidPl (cents1 _)) cards1 muln1.
rewrite (negbTE ntG) eqxx mul1n -(sdprod_card defG) (mulnC #|K|) expnM.
rewrite mulnA -expnMn big1 ?muln1 => [|A]; last first.
  by rewrite -negb_or -in_set2; move/out_m; rewrite /m => /= ->.
rewrite mulnC eq_sym (bigID (mem Dn)) /= mulnC.
rewrite big1 ?mul1n => [|A]; last by move/out_n->.
rewrite big_setU1 //= /n setU11 mul1n.
rewrite (eq_bigr (fun _ => #|'C_M(R)| ^ #|R|)%N) => [|A R_A]; last first.
  rewrite inE R_A orbT mul1n; case/imsetP: R_A => x Kx ->.
  suffices nMx: x \in 'N(M) by rewrite -{1}(normP nMx) centJ -conjIg !cardJg.
  exact: subsetP (subsetP sKG x Kx).
rewrite mulnC prod_nat_const card_orbit astab1JG.
have ->: 'N_K(R) = 1 by rewrite -(setIidPl sKG) -setIA -normD1 snRG tiKR.
rewrite indexg1 -expnMn eq_sym eqn_exp2r ?cardG_gt0 //; move/eqP=> eq_fix.
split=> // [regR | regK].
  rewrite centsC (sameP setIidPl eqP) eqEcard subsetIl /=.
  move: eq_fix; rewrite regR cards1 exp1n mul1n => <-.
  suffices ->: 'C_M(G) = 1 by rewrite cards1 exp1n mul1n.
  by apply/trivgP; rewrite -regR setIS ?centS //; case/sdprod_context: defG.
move: eq_fix; rewrite regK cards1 muln1 => <-.
suffices ->: 'C_M(G) = 1 by rewrite cards1 exp1n mul1n.
by apply/trivgP; rewrite -regK setIS ?centS.
Qed.

End Wielandt_Frobenius.

(* This is B & G, Theorem 3.10. *)
Theorem Frobenius_primact gT (G K R M : {group gT}) :
    [Frobenius G = K ><| R] -> solvable G ->
    G \subset 'N(M) -> solvable M -> M :!=: 1 ->
  (*1*) coprime #|M| #|G| ->
  (*2*) semiprime M R ->
  (*3*) 'C_M(K) = 1 ->
  [/\ prime #|R|,
      #|M| = (#|'C_M(R)| ^ #|R|)%N
    & cyclic 'C_M(R) -> K^`(1) \subset 'C_K(M)].
Proof.
move: {2}_.+1 (ltnSn #|M|) => n; elim: n => // n IHn in gT G K R M *.
rewrite ltnS => leMn frobG solG nMG solM ntM coMG primRM tcKM.
case: (Frobenius_Wielandt_fixpoint frobG nMG) => // _ _ /(_ tcKM) oM.
have [defG ntK ntR ltKG _]:= Frobenius_context frobG.
have Rpr: prime #|R|.
  have [R1 | [r r_pr]] := trivgVpdiv R; first by case/eqP: ntR.
  case/Cauchy=> // x Rx ox; pose R0 := <[x]>; pose G0 := K <*> R0.
  have [_ defKR nKR tiKR] := sdprodP defG.
  have sR0R: R0 \subset R by rewrite cycle_subG.
  have sG0G: G0 \subset G by rewrite /G0 -genM_join gen_subG -defKR mulgS.
  have nKR0 := subset_trans sR0R nKR; have nMG0 := subset_trans sG0G nMG.
  have ntx: <[x]> != 1 by rewrite cycle_eq1 -order_gt1 ox prime_gt1.
  have [tcRM | ntcRM] := eqVneq 'C_M(R) 1.
    by rewrite -cardG_gt1 oM tcRM cards1 exp1n in ntM.
  have frobG0: [Frobenius G0 = K ><| R0].
    apply/Frobenius_semiregularP=> // [|y /setD1P[nty x_y]].
      by apply: sdprodEY nKR0 (trivgP _); rewrite -tiKR setIS.
    by apply: (Frobenius_reg_ker frobG); rewrite !inE nty (subsetP sR0R).
  case: (Frobenius_Wielandt_fixpoint frobG0 nMG0 (coprimegS _ coMG)) => // _ _.
  move/(_ tcKM)/eqP; rewrite oM cent_cycle.
  rewrite primRM; last by rewrite !inE Rx andbT -cycle_eq1.
  by rewrite eqn_exp2l ?cardG_gt1 // -orderE ox => /eqP->.
split=> // cyc_cMR.
have nM_MG: M <*> G \subset 'N(M) by rewrite join_subG normG.
have [V minV sVM] := minnormal_exists ntM nM_MG.
have [] := minnormal_solvable minV sVM solM.
rewrite join_subG; case/andP=> nVM nVG ntV; case/is_abelemP=> [q q_pr abelV].
have coVG := coprimeSg sVM coMG; have solV := solvableS sVM solM.
have cVK': K^`(1) \subset 'C_K(V).
  case: (eqVneq 'C_V(R) 1) => [tcVR | ntcRV].
    case: (Frobenius_Wielandt_fixpoint frobG nVG) => // _.
    by move/(_ tcVR)=> cVK _; rewrite (setIidPl cVK) der_sub.
  have ocVR: #|'C_V(R)| = q.
    have [u def_u]: exists u, 'C_V(R) = <[u]>.
      by apply/cyclicP; apply: cyclicS (setSI _ sVM) cyc_cMR.
    rewrite def_u -orderE (abelem_order_p abelV) -?cycle_eq1 -?def_u //.
    by rewrite -cycle_subG -def_u subsetIl.
  apply: (Frobenius_prime_cent_prime _ defG _ _ abelV)  => //.
    by case/prime_FrobeniusP: frobG.
  by rewrite (coprime_p'group _ (abelem_pgroup abelV) ntV) // coprime_sym.
have cMK': K^`(1) / V \subset 'C_(K / V)(M / V).
  have [-> | ntMV] := eqVneq (M / V) 1.
    by rewrite subsetI cents1 quotientS ?der_sub.
  have coKR := Frobenius_coprime frobG.
  case/prime_FrobeniusP: frobG => //.
  case/sdprod_context=> nsKG sRG defKR nKR tiKR regR; have [sKG _] := andP nsKG.
  have nVK := subset_trans sKG nVG; have nVR := subset_trans sRG nVG.
  have RVpr: prime #|R / V|.
    rewrite card_quotient // -indexgI setIC coprime_TIg ?(coprimegS sRG) //.
    by rewrite indexg1.
  have frobGV: [Frobenius G / V = (K / V) ><| (R / V)].
    apply/prime_FrobeniusP; rewrite // -?cardG_gt1 ?card_quotient //.
      rewrite -indexgI setIC coprime_TIg ?(coprimegS sKG) //.
      by rewrite indexg1 cardG_gt1.
    rewrite -coprime_norm_quotient_cent ?(coprimegS sRG) //= regR quotient1.
    rewrite -defKR quotientMl // sdprodE ?quotient_norms //.
    by rewrite coprime_TIg ?coprime_morph.
  have ltMVn: #|M / V| < n by apply: leq_trans leMn; rewrite ltn_quotient.
  rewrite quotient_der //; move/IHn: frobGV.
  case/(_ _ ltMVn); rewrite ?quotient_sol ?quotient_norms ?coprime_morph //.
  - move=> Vx; case/setD1P=> ntVx; case/morphimP=> x nVx Rx defVx.
    rewrite defVx /= -cent_cycle -quotient_cycle //; congr 'C__(_ / V).
    apply/eqP; rewrite eqEsubset cycle_subG Rx /=.
    apply: contraR ntVx => /(prime_TIg Rpr)/trivgP.
    by rewrite defVx /= (setIidPr _) cycle_subG // => /set1P->; rewrite morph1.
  - rewrite -coprime_norm_quotient_cent ?(coprimegS sKG) ?(subset_trans sKG) //.
    by rewrite tcKM quotient1.
  move=> _ _ -> //; rewrite -coprime_quotient_cent ?quotient_cyclic //.
  by rewrite (coprimegS sRG).
have{cVK' cMK'} [[sK'K cVK'] [_ cMVK']] := (subsetIP cVK', subsetIP cMK').
have sK'G: K^`(1) \subset G by rewrite (subset_trans sK'K) ?proper_sub.
have coMK': coprime #|M| #|K^`(1)| := coprimegS sK'G coMG.
rewrite subsetI sK'K (stable_factor_cent cVK') //; apply/and3P; split=> //.
by rewrite commGC -quotient_cents2 // (subset_trans sK'G).
Qed.

End BGsection3.