path: root/mathcomp/odd_order/PFsection14.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 choice.
From mathcomp
Require Import fintype tuple finfun bigop prime binomial ssralg poly finset.
From mathcomp
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
From mathcomp
Require Import gfunctor gproduct center cyclic commutator gseries nilpotent.
From mathcomp
Require Import pgroup sylow hall abelian maximal frobenius.
From mathcomp
Require Import matrix mxalgebra mxrepresentation mxabelem vector.
From mathcomp
Require Import BGsection1 BGsection3 BGsection7.
From mathcomp
Require Import BGsection14 BGsection15 BGsection16 BGappendixC.
From mathcomp
Require Import ssrnum rat algC cyclotomic algnum.
From mathcomp
Require Import classfun character integral_char inertia vcharacter.
From mathcomp
Require Import PFsection1 PFsection2 PFsection3 PFsection4.
From mathcomp
Require Import PFsection5 PFsection6 PFsection7 PFsection8 PFsection9.
From mathcomp
Require Import PFsection10 PFsection11 PFsection12 PFsection13.

(******************************************************************************)
(* This file covers Peterfalvi, Section 14: Non_existence of G.               *)
(* It completes the proof of the Odd Order theorem.                           *)
(******************************************************************************)

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

Import GroupScope GRing.Theory FinRing.Theory Num.Theory.

Section Fourteen.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types (p q : nat) (x y z : gT).
Implicit Types H K L N P Q R S T U W : {group gT}.

Local Notation "#1" := (inord 1) (at level 0).

(* Supplementary results that apply to both S and T, but that are not         *)
(* formally stated as such; T, V, L, tau1L and phi are only used at the end   *)
(* of this section, to state and prove FTtype2_support_coherence.             *)
Section MoreSTlemmas.

Local Open Scope ring_scope.
Variables W W1 W2 S T U V L : {group gT}.
Variables (tau1L : {additive 'CF(L) -> 'CF(G)}) (phi : 'CF(L)).

(* Implicit (dependent) forward assuptions. *)
Hypotheses (defW : W1 \x W2 = W) (xdefW : W2 \x W1 = W) (maxL : L \in 'M).

Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
Local Notation P := `S`_\F%G.
Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
Local Notation PU := S^`(1)%G.
Local Notation "` 'PU'" := `S^`(1)%g (at level 0) : group_scope.
Local Notation "` 'L'" := (gval L) (at level 0, only parsing).
Local Notation H := `L`_\F%G.
Local Notation "` 'H'" := `L`_\F%g (at level 0, format "` 'H'") : group_scope.

Let p := #|W2|.
Let q := #|W1|.
Let u := #|U|.
Let v := #|V|.
Let h := #|H|.
Let e := #|L : H|.
Let ccG A := class_support A G.

Let calL := seqIndD H L H 1.
Let betaL := 'Ind[L, H] 1 - phi.
Local Notation tauL := (FT_DadeF maxL).

(* Explicit (non-dependent) forward assumptions. *)
Hypotheses (StypeP : of_typeP S U defW) (TtypeP : of_typeP T V xdefW).
Hypothesis (cohL : coherent_with calL L^# tauL tau1L) (Lphi : phi \in calL).

(* The remaining assumptions can be generated as backchaining gools. *)
Hypotheses (maxS : S \in 'M) (maxT : T \in 'M).

Let pddS := FT_prDade_hypF maxS StypeP.
Let pddT := FT_prDade_hypF maxT TtypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddS.
Let sigma := cyclicTIiso ctiWG.
Let w_ i j := cyclicTIirr defW i j.

(* An inequality used in the proof of (14.11.4), at the bottom of page 90, to *)
(* show that 1/uq and 1/vp are less that 1/2q^2 (so Wn is either W1 or W2).   *)
Lemma FTtypeP_complV_ltr (Wn : {group gT}) :
  (#|Wn| <= q)%N -> (u * q)%:R^-1 < (2 * #|Wn| ^ 2)%:R^-1 :> algC.
Proof.
move=> leWn_q; rewrite !natrM ltf_pinv ?rpredM ?qualifE ?gt0CG ?ltr0n //.
rewrite -!natrM ltr_nat (@leq_ltn_trans (2 * q ^ 2)) ?mulnA ?leq_mul // mul2n.
have: [Frobenius U <*> W1 = U ><| W1] by have [[]] := FTtypeP_facts maxS StypeP.
by move/ltn_odd_Frobenius_ker/implyP; rewrite mFT_odd ltn_pmul2r ?cardG_gt0.
Qed.

(* This formalizes the loose symmetry used in (14.11.3) to show that #[g] is  *)
(* coprime to pq.                                                             *)
Lemma coprime_typeP_Galois_core g :
  typeP_Galois StypeP -> g \notin ccG W^# -> g \notin ccG P^# -> coprime #[g] p.
Proof.
move=> galS W'g; apply: contraR => p_g.
have ntg: g != 1%g by apply: contraNneq p_g => ->; rewrite order1 coprime1n.
have [pr_q pr_p]: prime q /\ prime p := FTtypeP_primes maxS StypeP.
have [[_ hallW1 _ defS] [_ _ _ defPU] _ [_ _ sW2P _ regPUW1] _] := StypeP.
have coPUq: coprime #|PU| q by rewrite (coprime_sdprod_Hall_r defS).
have [[_ _ nPUW1 _] [_ _ nPU _]] := (sdprodP defS, sdprodP defPU).
have ntP: P :!=: 1%g := mmax_Fcore_neq1 maxS.
have frobPU: [Frobenius PU = P ><| U].
  have notS5 := FTtype5_exclusion maxS.
  have inN1 x: x \in 'N(1) by rewrite norm1 inE.
  have [_ ntU _ _] := compl_of_typeII_IV maxS StypeP notS5.
  have [] := typeP_Galois_P maxS notS5 galS; rewrite Ptype_factor_prime //.
  rewrite (group_inj (Ptype_Fcore_kernel_trivial _ _)) // => F [fP [fU _]].
  rewrite Ptype_Fcompl_kernel_trivial //.
  case=> /trivgP injfU fJ [_ /isomP[injfP _] _] _.
  apply/Frobenius_semiregularP=> // y /setD1P[nty Uy].
  apply/trivgP/subsetP=> x /setIP[Px /cent1P-cxy]; apply: contraR nty.
  rewrite -(morph_injm_eq1 injfU) // -val_eqE -(cosetpre1 1) !(inN1, inE) /=.
  rewrite -(morph_injm_eq1 injfP) ?mem_quotient //= => /mulfI/inj_eq <-.
  rewrite mulr1 -[_ * _]fJ ?mem_quotient //= qactE ?dom_qactJ //=.
  by rewrite conjgE cxy mulKg.
have pP: p.-group P by have [_ [/andP[]]] := FTtypeP_facts _ StypeP.
have{p_g}[y [a P1a cagy]]: exists y, exists2 a, a \in P^# & g ^ y \in 'C[a].
  have sylP: p.-Sylow(G) P.
    have [/Hall_pi/= hallP _ _] := FTcore_facts maxS; apply: etrans hallP.
    have [_ _ [n ->]] := pgroup_pdiv pP (mmax_Fcore_neq1 maxS).
    by apply/eq_pHall => r1; rewrite pi_of_exp ?pi_of_prime.
  have [y _ Pa] := Sylow_Jsub sylP (subsetT _) (p_elt_constt p g).
  pose a := g.`_p ^ y; have{Pa} Pa: a \in P by rewrite -cycle_subG cycleJ.
  exists y, a; last by rewrite cent1C /a conjXg groupX ?cent1id.
  rewrite !inE conjg_eq1 (contraNneq _ p_g) // => /constt1P/p'nat_coprime-> //.
  exact: pnat_id.
have /(mem_sdprod defS)[x [w [PUx W1w Dgy _]]]: g ^ y \in S.
  have A0a: a \in 'A0(S) := subsetP (Fcore_sub_FTsupp0 maxS) a P1a.
  have [_ _ _ _ [tiA0 _]] := FTtypeP_facts _ StypeP.
  by rewrite (subsetP (cent1_normedTI tiA0 A0a)) // 2!inE.
suffices w_eq1: w = 1%g.
  have sCaP: 'C_PU[a] \subset P := Frobenius_cent1_ker frobPU P1a.
  rewrite -[g](conjgK y) mem_imset2 ?inE //= conjg_eq1 ntg /=.
  by rewrite (subsetP sCaP) // inE cagy Dgy w_eq1 mulg1 PUx.
apply: contraNeq W'g => ntw; have nPUw := subsetP nPUW1 w W1w.
have{x PUx Dgy} /imset2P[x z W2w_x _ Dgy]: g ^ y \in class_support (W2 :* w) PU.
  rewrite -(regPUW1 w) ?inE ?ntw // class_supportEr -cover_imset.
  have coPUw := coprime_dvdr (order_dvdG W1w) coPUq.
  have [/cover_partition-> _] := partition_cent_rcoset nPUw coPUw.
  by rewrite Dgy mem_rcoset mulgK.
rewrite -[g](conjgK (y * z^-1)%g) mem_imset2 ?inE //= conjg_eq1 ntg /= conjgM.
by rewrite Dgy conjgK -(dprodWC defW) -[x](mulgKV w) mem_mulg -?mem_rcoset.
Qed.

Hypothesis Stype2 : FTtype S == 2.

(* This is used to bound #|ccG P^#| and #|ccG Q^#| in the proof of (14.11.4). *)
Lemma FTtype2_cc_core_ler : #|G|%:R^-1 * #|ccG P^#|%:R <= (u * q)%:R^-1 :> algC.
Proof.
have ->: (u * q)%:R^-1 = #|S|%:R^-1 * #|P|%:R :> algC.
  have [[_ _ _ /sdprod_card <-] [_ _ _ /sdprod_card <-] _ _ _] := StypeP.
  by rewrite mulrC -mulnA [in RHS]natrM invfM mulVKf ?neq0CG.
have [_ _] := FTtypeII_ker_TI maxS Stype2; rewrite FTsupp1_type2 // => tiP1.
rewrite {tiP1}(card_support_normedTI tiP1) natrM natf_indexg ?subsetT //.
rewrite mulrCA mulKf ?neq0CG // mulrC ler_pmul2l ?invr_gt0 ?gt0CG // leC_nat.
by rewrite cardsDS ?sub1G ?leq_subr.
Qed.

Hypotheses (maxNU_L : L \in 'M('N(U))) (phi1 : phi 1%g = e%:R).

(* This is Peterfalvi (14.11.2), stated for S and L rather than T and M; it  *)
(* is loosely used in this form at the very end of the proof of (14.16).     *)
Lemma FTtype2_support_coherence :
    (u.-1 %/ q < h.-1 %/ e)%N -> (v.-1 %/ p < h.-1 %/ e)%N -> 
  [/\ e = (p * q)%N
    & exists nb, exists2 chi, chi = tau1L phi \/ chi = - tau1L phi^*%CF
    & tauL betaL = \sum_ij (-1)^+ nb ij *: sigma 'chi_ij - chi].
Proof.
move=> ub_u ub_v; have nsHL : H <| L := gFnormal _ _.
have pairST := of_typeP_pair maxS StypeP maxT TtypeP.
have [//|frobL sUH defL] := FTtypeII_support_facts maxS StypeP _ pairST maxNU_L.
have Ltype1 := FT_Frobenius_type1 maxL frobL.
have irr_phi: phi \in irr L by apply: FTtype1_Ind_irr Lphi.
have betaL_P := FTtypeI_bridge_facts _ _ Ltype1 cohL Lphi phi1.
have e_dv_h1: e %| h.-1 by apply: Frobenius_ker_dvd_ker1.
pose a i j := '[tauL betaL, sigma (w_ i j)].
have a0j j: j != 0 -> (a 0 j == 1 %[mod 2])%C.
  rewrite /a => nz_j; case/betaL_P: StypeP => _ _ -> //.
  by case=> [[_ /idPn[]] | [//]]; rewrite -natf_div // leC_nat -ltnNge.
have ai0 i: i != 0 -> (a i 0 == 1 %[mod 2])%C.
  rewrite /a (cycTIisoC _ pddT) => nz_i; case/betaL_P: TtypeP => _ _ -> //.
  by case=> [[_ /idPn[]] | [//]]; rewrite -natf_div // leC_nat -ltnNge.
have HbetaL: betaL \in 'CF(L, H^#) by apply: cfInd1_sub_lin_on Lphi phi1.
have betaL_W_0: {in cyclicTIset defW, tauL betaL =1 \0}.
  move=> z; case/betaL_P: StypeP => tiAM_W _ _ _.
  rewrite !inE -(setCK W) inE => /andP[_]; apply: cfun_onP z.
  apply: cfun_onS (Dade_cfunS _ _); rewrite FT_DadeF_supportE -disjoints_subset.
  rewrite -FTsupp_Frobenius // -setI_eq0 -subset0 -tiAM_W setIS //.
  by rewrite setUC subsetU ?sub_class_support.
have calL_gt1: (1 < size calL)%N.
  by apply: seqInd_nontrivial Lphi; rewrite ?mFT_odd.
have [] := Dade_Ind1_sub_lin cohL calL_gt1 irr_phi Lphi phi1; rewrite -/betaL.
rewrite -/calL odd_Frobenius_index_ler ?mFT_odd //= -/e -/h.
case=> _ a00 ZbetaL [Gamma [o_tau1_Ga o_1_Ga [aa Zaa Dbeta] []// _ ubGa _]].
have{a00} a00: a 0 0 = 1 by rewrite /a /w_ cycTIirr00 cycTIiso1.
have{a0j ai0} a_odd i j: (a i j == 1 %[mod 2])%C.
  have [[-> | /ai0 ai01] [-> | /a0j a0j1] //] := (eqVneq i 0, eqVneq j 0).
    by rewrite a00 (eqCmod_nat 2 1 1).
  by rewrite -(eqCmodDr _ 1) -{1}a00 cycTIiso_cfdot_exchange // eqCmodD.
have [_ o_tauLeta _ _] := FTtypeI_bridge_facts _ StypeP Ltype1 cohL Lphi phi1.
pose etaW := map sigma (irr W).
have o1eta: orthonormal etaW := cycTIiso_orthonormal _.
have [X etaX [Y [defGa oXY oYeta]]] := orthogonal_split etaW (Gamma + 1).
have lbY: 0 <= '[Y] ?= iff (Y == 0).
  by split; rewrite ?cfnorm_ge0 // eq_sym cfnorm_eq0.
have [b Db defX] := orthonormal_span o1eta etaX.
do [rewrite addrC !addrA addrAC -addrA; set Z := _ - _] in Dbeta.
have oZeta: orthogonal Z etaW.
  apply/orthoPl=> xi /memv_span; apply: {xi}(span_orthogonal o_tauLeta).
  rewrite rpredB ?rpredZ ?big_seq ?rpred_sum ?memv_span ?map_f // => xi Lxi.
  by rewrite rpredZ ?memv_span ?map_f.
have lb_b ij (b_ij := b (sigma 'chi_ij)):
  1 <= `|b_ij| ^+ 2 ?= iff [exists n : bool, b_ij == (-1) ^+ n].
- have /codomP[[i j] Dij] := dprod_Iirr_onto defW ij.
  have{b_ij} ->: b_ij = a i j.
    rewrite /a /w_ -Dij Dbeta defGa 2!cfdotDl. 
    have ->: '[X, sigma 'chi_ij] = b_ij by rewrite /b_ij Db.
    by rewrite (orthoPl oYeta) ?(orthoPl oZeta) ?map_f ?mem_irr // !addr0.
  have Zaij: a i j \in Cint by rewrite Cint_cfdot_vchar ?cycTIiso_vchar.
  rewrite Cint_normK //; split.
    rewrite sqr_Cint_ge1 //; apply: contraTneq (a_odd i j) => ->.
    by rewrite (eqCmod_nat 2 0 1).
  apply/eqP/exists_eqP=> [a2_1|[n ->]]; last by rewrite sqrr_sign.
  rewrite (CintEsign Zaij) normC_def conj_Cint // -expr2 -a2_1 sqrtC1 mulr1.
  by exists (a i j < 0).
have ub_e: e%:R <= #|Iirr W|%:R ?= iff (e == p * q)%N :> algC.
  rewrite lerif_nat card_Iirr_cyclic //; last by have [] := ctiWG.
  rewrite -(dprod_card xdefW); apply: leqif_eq.
  case: defL => [|[y Qy]] defL; rewrite /e -(index_sdprod defL).
    by rewrite leq_pmull ?cardG_gt0.
  suffices /normP <-: y \in 'N(W1).
    by rewrite -conjYg !cardJg (dprodWY defW) -(dprod_card xdefW).
  have cQQ: abelian T`_\F by have [_ [/and3P[]]] := FTtypeP_facts maxT TtypeP.
  have sW1Q: W1 \subset T`_\F by have [_ _ _ []] := TtypeP.
  by rewrite (subsetP _ y Qy) // sub_abelian_norm.
have /(_ predT) := lerif_add (lerif_sum (in1W lb_b)) lbY.
rewrite sumr_const addr0 => /(lerif_trans ub_e)/ger_lerif/esym.
have ->: \sum_i `|b (sigma 'chi_i)| ^+ 2 = '[X].
  rewrite defX cfnorm_sum_orthonormal // big_map (big_nth 0) big_mkord.
  by rewrite size_tuple; apply: eq_bigr => ij _; rewrite -tnth_nth.
rewrite -cfnormDd // -defGa cfnormDd // cfnorm1 -ler_subr_addr ubGa.
case/and3P=> /eqP-De /'forall_exists_eqP/fin_all_exists[/= n Dn] /eqP-Y0.
pose chi := X - tauL betaL; split=> //; exists n, chi; last first.
  apply: canRL (addrK _) _; rewrite addrC subrK defX big_map (big_nth 0).
  by rewrite big_mkord size_tuple; apply: eq_bigr => ij; rewrite -tnth_nth Dn.
have Z1chi: chi \in dirr G.
  rewrite dirrE rpredB //=; last first.
    rewrite defX big_map (big_nth 0) big_mkord size_tuple rpred_sum //= => ij.
    have [_ Zsigma] := cycTI_Zisometry ctiWG.
    by rewrite -tnth_nth Dn rpredZsign ?Zsigma ?irr_vchar.
  apply/eqP/(addIr '[X]); rewrite -cfnormBd; last first.
    rewrite /chi Dbeta defGa Y0 addr0 opprD addNKr cfdotNl.
    by rewrite (span_orthogonal oZeta) ?oppr0 // memv_span ?mem_head.
  rewrite addrAC subrr add0r cfnormN Dade_isometry // cfnormBd; last first.
    by rewrite cfdotC (seqInd_ortho_Ind1 _ _ Lphi) ?conjC0.
  rewrite cfnorm_Ind_cfun1 // -/e irrWnorm // addrC; congr (1 + _).
  rewrite defX cfnorm_sum_orthonormal // big_map big_tuple.
  rewrite De (dprod_card xdefW) -card_Iirr_cyclic //; last by have[]:= ctiWG.
  by rewrite -sumr_const; apply: eq_bigr => ij _; rewrite Dn normr_sign expr1n.
have [[Itau1 Ztau1] Dtau1] := cohL.
suffices /cfdot_add_dirr_eq1: '[tau1L phi - tau1L phi^*%CF, chi] = 1.
  rewrite -(cfConjC_Dade_coherent cohL) ?mFT_odd // rpredN dirr_aut.
  by apply; rewrite // dirrE Ztau1 ?Itau1 ?mem_zchar ?irrWnorm /=.
rewrite cfdotBr (span_orthogonal o_tauLeta) ?add0r //; last first.
  by rewrite rpredB ?memv_span ?map_f ?cfAut_seqInd.
have Zdphi := seqInd_sub_aut_zchar nsHL conjC Lphi.
rewrite -raddfB Dtau1 ?zcharD1_seqInd // Dade_isometry ?(zchar_on Zdphi) //. 
rewrite cfdotBr !cfdotBl cfdot_conjCl cfAutInd rmorph1 irrWnorm //.
rewrite (seqInd_ortho_Ind1 _ _ Lphi) // conjC0 subrr add0r opprK.
by rewrite cfdot_conjCl (seqInd_conjC_ortho _ _ _ Lphi) ?mFT_odd ?conjC0 ?subr0.
Qed.

End MoreSTlemmas.

Section NonconjType1.
(* Properties of non-conjugate type I groups, used symmetrically for L and M  *)
(* in the proofs of (14.14) and (14.16).                                      *)

Local Open Scope ring_scope.
Variables (M L : {group gT}) (phi : 'CF(L)) (psi : 'CF(M)).
Variable (tau1L : {additive 'CF(L) -> 'CF(G)}).
Variable (tau1M : {additive 'CF(M) -> 'CF(G)}).
Hypotheses (maxL : L \in 'M) (maxM : M \in 'M).
Let ddL := FT_DadeF_hyp maxL.
Let ddM := FT_DadeF_hyp maxM.
Let tauL := Dade ddL.
Let tauM := Dade ddM.
Let H := L`_\F%G.
Let K := M`_\F%G.
Let calL := seqIndD H L H 1.
Let calM := seqIndD K M K 1.
Let u : algC := #|L : H|%:R.
Let v : algC := #|M : K|%:R.
Let betaL := 'Ind[L, H] 1 - phi.
Let a := '[tauL betaL, tau1M psi].

Hypothesis (cohL : coherent_with calL L^# tauL tau1L).
Hypothesis (cohM : coherent_with calM M^# tauM tau1M).
Hypotheses (Lphi : phi \in calL) (Mpsi : psi \in calM).
Hypotheses (phi1 : phi 1%g = u) (psi1 : psi 1%g = v).
Hypotheses (Ltype1 : FTtype L == 1%N) (Mtype1 : FTtype M == 1%N).
Hypothesis not_MG_L : gval L \notin M :^: G.

Let irrL := FTtype1_Ind_irr maxL Ltype1.
Let irrM := FTtype1_Ind_irr maxM Mtype1.

Lemma disjoint_Dade_FTtype1 : [disjoint Dade_support ddM & Dade_support ddL].
Proof.
by rewrite !FT_DadeF_supportE -!FTsupp1_type1 ?FT_Dade1_support_disjoint.
Qed.
Let TItauML := disjoint_Dade_FTtype1.

Lemma coherent_FTtype1_ortho : orthogonal (map tau1M calM) (map tau1L calL).
Proof.
apply/orthogonalP=> _ _ /mapP[xiM Mxi ->] /mapP[xiL Lxi ->].
have [irrLxi irrMxi] := (irrL Lxi, irrM Mxi).
exact: (disjoint_coherent_ortho (mFT_odd _) _ cohM cohL).
Qed.
Let oML := coherent_FTtype1_ortho.

(* This is the inequality used in both branches of (14.14). *)
Lemma coherent_FTtype1_core_ltr : a != 0 -> #|K|.-1%:R / v <= u - 1.
Proof.
have [nsHL nsKM]: H <| L /\ K <| M by rewrite !gFnormal.
have [irr_phi irr_psi] := (irrL Lphi, irrM Mpsi).
have frobL: [Frobenius L with kernel H] := FTtype1_Frobenius maxL Ltype1.
have [[Itau1 Ztau1] Dtau1] := cohM.
have o1M: orthonormal (map tau1M calM).
  apply: map_orthonormal Itau1 _.
  exact: sub_orthonormal (undup_uniq _) (irr_orthonormal M).
have Lgt1: (1 < size calL)%N by apply: seqInd_nontrivial (mFT_odd _ ) _ Lphi.
have [[_ _]] := Dade_Ind1_sub_lin cohL Lgt1 irr_phi Lphi phi1.
rewrite -/tauL -/betaL -/calL => ZbetaL [Gamma [_ _ [b _ Dbeta]]]. 
rewrite odd_Frobenius_index_ler ?mFT_odd // -/u => -[]// [_ ub_Ga] _ nz_a.
have Za: a \in Cint by rewrite Cint_cfdot_vchar // ?Ztau1 ?mem_zchar.
have [X M_X [Del [defGa oXD oDM]]] := orthogonal_split (map tau1M calM) Gamma.
apply: ler_trans ub_Ga; rewrite defGa cfnormDd // ler_paddr ?cfnorm_ge0 //.
suffices ->: '[X] = (a / v) ^+ 2 * (\sum_(xi <- calM) xi 1%g ^+ 2 / '[xi]).
  rewrite sum_seqIndC1_square // -(natrB _ (cardG_gt0 K)) subn1.
  rewrite exprMn !mulrA divfK ?neq0CiG // mulrAC -mulrA.
  by rewrite ler_pemull ?sqr_Cint_ge1 // divr_ge0 ?ler0n.
have [_ -> defX] := orthonormal_span o1M M_X.
have Mgt1: (1 < size calM)%N by apply: seqInd_nontrivial (mFT_odd _ ) _ Mpsi.
have [[oM1 _ _] _ _] := Dade_Ind1_sub_lin cohM Mgt1 irr_psi Mpsi psi1.
rewrite exprMn -(Cint_normK Za) -[v]normr_nat -normfV -/v mulr_sumr.
rewrite defX cfnorm_sum_orthonormal // big_map; apply: eq_big_seq => xi Mxi.
have Zxi1 := Cint_seqInd1 Mxi; rewrite -(Cint_normK Zxi1) -(conj_Cint Zxi1).
rewrite irrWnorm ?irrM // divr1 -!exprMn -!normrM; congr (`|_| ^+ 2).
rewrite -mulrA mulrC -mulrA; apply: canRL (mulKf (neq0CiG _ _)) _.
rewrite -(canLR (addrK _) defGa) cfdotBl (orthoPl oDM) ?map_f // subr0.
rewrite -(canLR (addKr _) Dbeta) cfdotDl cfdotNl cfdotC cfdotDr cfdotBr.
rewrite (orthoPr oM1) ?map_f // (orthogonalP oML) ?map_f // subrr add0r.
rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 ?oppr0 => [|nu Mnu]; last first.
  by rewrite cfdotZr (orthogonalP oML) ?map_f ?mulr0.
apply/eqP; rewrite conjC0 oppr0 add0r -subr_eq0 -conjC_nat -!cfdotZr.
rewrite -raddfZnat -raddfZ_Cint // -cfdotBr -raddfB -/v -psi1.
rewrite Dtau1 ?zcharD1_seqInd ?sub_seqInd_zchar //.
rewrite (cfdotElr (Dade_cfunS _ _) (Dade_cfunS _ _)) setIC.
by have:= TItauML; rewrite -setI_eq0 => /eqP->; rewrite big_set0 mulr0.
Qed.

End NonconjType1.

(* This is the context associated with Hypothesis (13.1). *)
Variables S T U V W W1 W2 : {group gT}.
Hypotheses (defW : W1 \x W2 = W) (xdefW : W2 \x W1 = W).
Hypotheses (pairST : typeP_pair S T defW) (maxS : S \in 'M) (maxT : T \in 'M).
Hypotheses (StypeP : of_typeP S U defW) (TtypeP : of_typeP T V xdefW).

Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
Local Notation What := (cyclicTIset defW).

Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
Local Notation P := `S`_\F%G.
Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
Local Notation PU := S^`(1)%G.
Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.

Local Notation "` 'T'" := (gval T) (at level 0, only parsing) : group_scope.
Local Notation Q := `T`_\F%G.
Local Notation "` 'Q'" := `T`_\F (at level 0) : group_scope.
Local Notation QV := T^`(1)%G.
Local Notation "` 'QV'" := `T^`(1) (at level 0) : group_scope.
Local Notation "` 'V'" := (gval V) (at level 0, only parsing) : group_scope.

Let defS : PU ><| W1 = S. Proof. by have [[]] := StypeP. Qed.
Let defPU : P ><| U = PU. Proof. by have [_ []] := StypeP. Qed.

Let defT : QV ><| W2 = T. Proof. by have [[]] := TtypeP. Qed.
Let defQV : Q ><| V = QV. Proof. by have [_ []] := TtypeP. Qed.

Let notStype1 : FTtype S != 1%N. Proof. exact: FTtypeP_neq1 StypeP. Qed.
Let notStype5 : FTtype S != 5%N. Proof. exact: FTtype5_exclusion maxS. Qed.

Let pddS := FT_prDade_hypF maxS StypeP.
Let ptiWS : primeTI_hypothesis S PU defW := FT_primeTI_hyp StypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddS.

Let pddT := FT_prDade_hypF maxT TtypeP.
Let ptiWT : primeTI_hypothesis T QV xdefW := FT_primeTI_hyp TtypeP.

Let ntW1 : W1 :!=: 1. Proof. by have [[]] := StypeP. Qed.
Let ntW2 : W2 :!=: 1. Proof. by have [_ _ _ []] := StypeP. Qed.
Let cycW1 : cyclic W1. Proof. by have [[]] := StypeP. Qed.
Let cycW2 : cyclic W2. Proof. by have [_ _ _ []] := StypeP. Qed.

Let p := #|W2|.
Let q := #|W1|.
Let u := #|U|.
Let v := #|V|.
Let nU := (p ^ q).-1 %/ p.-1.
Let nV := (q ^ p).-1 %/ q.-1.

Let pr_p : prime p. Proof. by have [] := FTtypeP_primes maxS StypeP. Qed.
Let pr_q : prime q. Proof. by have [] := FTtypeP_primes maxS StypeP. Qed.

Local Open Scope ring_scope.

Let qgt2 : (q > 2)%N. Proof. by rewrite odd_gt2 ?mFT_odd ?cardG_gt1. Qed.
Let pgt2 : (p > 2)%N. Proof. by rewrite odd_gt2 ?mFT_odd ?cardG_gt1. Qed.

Let coPUq : coprime #|PU| q.
Proof. by rewrite (coprime_sdprod_Hall_r defS); have [[]] := StypeP. Qed.

Let nirrW1 : #|Iirr W1| = q. Proof. by rewrite card_Iirr_cyclic. Qed.
Let nirrW2 : #|Iirr W2| = p. Proof. by rewrite card_Iirr_cyclic. Qed.
Let NirrW1 : Nirr W1 = q. Proof. by rewrite -nirrW1 card_ord. Qed.
Let NirrW2 : Nirr W2 = p. Proof. by rewrite -nirrW2 card_ord. Qed.

Let sigma := (cyclicTIiso ctiWG).
Let w_ i j := (cyclicTIirr defW i j).
Local Notation eta_ i j := (sigma (w_ i j)).

Local Notation Imu2 := (primeTI_Iirr ptiWS).
Let mu2_ i j := primeTIirr ptiWS i j.
Let mu_ := primeTIred ptiWS.
Local Notation chi_ j := (primeTIres ptiWS j).

Local Notation Inu2 := (primeTI_Iirr ptiWT).
Let nu2_ i j := primeTIirr ptiWT j i.
Let nu_ := primeTIred ptiWT.

Local Notation tauS := (FT_Dade0 maxS).
Local Notation tauT := (FT_Dade0 maxT).

Let calS0 := seqIndD PU S S`_\s 1.
Let rmR_S := FTtypeP_coh_base maxS StypeP.
Let scohS0 : subcoherent calS0 tauS rmR_S.
Proof. exact: FTtypeP_subcoherent StypeP. Qed.

Let calS := seqIndD PU S P 1.
Let sSS0 : cfConjC_subset calS calS0.
Proof. exact/seqInd_conjC_subset1/Fcore_sub_FTcore. Qed.

Let calT := seqIndD QV T Q 1.

(* This is Hypothesis (14.1). *)
Hypothesis ltqp: (q < p)%N.

(* This corresponds to Peterfalvi, Theorem (14.2). *)
(* As we import the conclusion of BGappendixC, which covers Appendix C of the *)
(* Bender and Glauberman text, we can state this theorem negatively. This     *)
(* will avoid having to repeat its statement thoughout the proof : we will    *)
(* simply end each nested set of assumptions (corresponding to (14.3) and     *)
(* (14.10)) with a contradiction.                                             *)
Theorem no_full_FT_Galois_structure :
 ~ [/\ (*a*) exists Fpq : finFieldImage P W2 U,
               [/\ #|P| = (p ^ q)%N, #|U| = nU & coprime nU p.-1]
    & (*b*) [/\ q.-abelem Q, W2 \subset 'N(Q)
              & exists2 y, y \in Q & W2 :^ y \subset 'N(U)]].
Proof.
case=> [[Fpq [oP oU coUp1]] [abelQ nQW2 nU_W2Q]].
have /idPn[] := ltqp; rewrite -leqNgt.
exact: (prime_dim_normed_finField _ _ _ defPU) nU_W2Q.
Qed.

(* Justification for Hypothesis (14.3). *)
Fact FTtypeP_max_typeII : FTtype S == 2.
Proof. by have [[_ ->]] := FTtypeP_facts maxS StypeP. Qed.
Let Stype2 := FTtypeP_max_typeII.

(* These correspond to Peterfalvi, Hypothesis (14.3). *)
Variables (L : {group gT}) (tau1L : {additive 'CF(L) -> 'CF(G)}) (phi : 'CF(L)).
Local Notation "` 'L'" := (gval L) (at level 0, only parsing).
Local Notation H := `L`_\F%G.
Local Notation "` 'H'" := `L`_\F%g (at level 0, format "` 'H'") : group_scope.

Hypothesis maxNU_L : L \in 'M('N(U)).

(* Consequences of the above. *)
Hypotheses (maxL : L \in 'M) (sNUL : 'N(U) \subset L) (sUH : U \subset H).
Hypotheses (frobL : [Frobenius L with kernel H]) (Ltype1 : FTtype L == 1%N).

Let calL := seqIndD H L H 1.
Local Notation tauL := (FT_DadeF maxL).
Let nsHL : H <| L. Proof. exact: gFnormal. Qed.
Let irrL : {subset calL <= irr L}. Proof. exact: FTtype1_Ind_irr. Qed.

Hypothesis cohL : coherent_with calL L^# tauL tau1L.
Hypotheses (Lphi : phi \in calL) (phi1 : phi 1%g = #|L : H|%:R).

Let betaS := FTtypeP_bridge StypeP #1.
Let betaT := FTtypeP_bridge TtypeP #1.
Let betaL := 'Ind[L, H] 1 - phi.

(* This is the first assertion of Peterfalvi (14.4). *)
Let galT : typeP_Galois TtypeP.
Proof.
apply: contraLR ltqp => /(FTtypeP_nonGalois_facts maxT)[].
by rewrite -/p -leqNgt => ->.
Qed.

(* This is the second assertion of Peterfalvi (14.4). *)
Let oV : v = nV.
Proof.
rewrite /v (card_FTtypeP_Galois_compl maxT galT) -/nV.
by rewrite !modn_small ?gtn_eqF // ltnW.
Qed.

(* This is Peterfalvi (14.5). *)
Let defL : exists2 y, y \in Q & H ><| (W1 <*> W2 :^ y) = L.
Proof.
have [//|_ _ []// defL] := FTtypeII_support_facts maxS StypeP _ pairST maxNU_L.
have [_ _ /negP[]] := compl_of_typeII maxS StypeP Stype2.
have [_ _ _] := FTtypeI_bridge_facts maxS StypeP Ltype1 cohL Lphi phi1.
case=> [[_ ubH] | [_ /idPn[]]]; last by rewrite -(index_sdprod defL) -ltnNge.
have{ubH} /eqP defH: `H == U.
  rewrite eq_sym eqEcard sUH /= -(prednK (cardG_gt0 U)) -add1n -leq_subLR subn1.
  have [_ _ _ _ /divnK <-] := FTtypeP_bridge_facts maxS StypeP.
  by rewrite -leC_nat natrM -ler_pdivr_mulr ?gt0CG // {1}(index_sdprod defL).
rewrite (subset_trans sNUL) // -(sdprodW defL) -(sdprodW defS) mulSg //.
by rewrite -(sdprodW defPU) defH mulG_subr.
Qed.

Let indexLH : #|L : H| = (p * q)%N.
Proof.
have [y Qy /index_sdprod <-] := defL; rewrite (dprod_card xdefW).
suffices /normP <-: y \in 'N(W1) by rewrite -conjYg cardJg (dprodWY defW).
have cQQ: abelian Q by have [_ [/and3P[]]] := FTtypeP_facts _ TtypeP.
by apply: (subsetP (sub_abelian_norm cQQ _)) => //; have [_ _ _ []] := TtypeP.
Qed.

(* This is Peterfalvi (14.6). *)
Let galS : typeP_Galois StypeP.
Proof.
apply/idPn=> gal'S; have [q3 oU] := FTtypeP_nonGalois_facts maxS gal'S.
have [H1 [_ _ _ _]] := typeP_Galois_Pn maxS (FTtype5_exclusion maxS) gal'S.
rewrite def_Ptype_factor_prime // Ptype_Fcompl_kernel_trivial // -/p q3 /=.
set a := #|U : _| => [] [a_gt1 a_dv_p1 _ [U1 isoU1]].
have{isoU1} isoU: U \isog U1 := isog_trans (quotient1_isog U) isoU1.
have{a_gt1 a_dv_p1} defU1: U1 :=: [set: 'rV_2].
  apply/eqP; rewrite eqEcard subsetT -(card_isog isoU) oU.
  rewrite cardsT card_matrix card_ord Zp_cast // leq_sqr -/p.
  apply: dvdn_leq; first by rewrite -(subnKC pgt2).
  rewrite -divn2 -(@Gauss_dvdl a _ 2) ?divnK //.
    by rewrite dvdn2 -subn1 odd_sub ?odd_gt0 ?mFT_odd.
  by rewrite coprimen2 (dvdn_odd (dvdn_indexg U _)) ?mFT_odd.
have [r pr_r r_r_U] := rank_witness U.
have [R0 sylR0] := Sylow_exists r U; have [sR0U rR0 _] := and3P sylR0.
have [R sylR sR0R] := Sylow_superset (subset_trans sR0U sUH) rR0.
have [sRH rR _] := and3P sylR.
have cUU: abelian U by have [[]] := FTtypeP_facts maxS StypeP.
have tiA0: normedTI 'A0(S) G S by have [_ _ _ _ []] := FTtypeP_facts _ StypeP.
have [_ sUPU _ nPU _] := sdprod_context defPU.
have coPU := coprimegS (joing_subl U W1) (Ptype_Fcore_coprime StypeP).
have abR0: abelian R0 := abelianS sR0U cUU.
have{a U1 defU1 isoU r_r_U} rR0_2: 'r(R0) = 2.
  by rewrite (rank_Sylow sylR0) -r_r_U (isog_rank isoU) defU1 rank_mx_group.
have piUr: r \in \pi(U) by rewrite -p_rank_gt0 -(rank_Sylow sylR0) rR0_2.
have /exists_inP[x /setD1P[ntx R0x] ntCPx]: [exists x in R0^#, 'C_P[x] != 1%g].
  have ncycR0: ~~ cyclic R0 by rewrite abelian_rank1_cyclic ?rR0_2.
  have coPR0: coprime #|P| #|R0| := coprimegS sR0U coPU.
  rewrite -negb_forall_in; apply: contra (mmax_Fcore_neq1 maxS) => regR0P.
  rewrite -subG1 -(coprime_abelian_gen_cent1 abR0 _ (subset_trans sR0U nPU)) //.
  by rewrite gen_subG; apply/bigcupsP=> x /(eqfun_inP regR0P)->.
have{x ntx R0x ntCPx} sZR_R0: 'Z(R) \subset R0.
  have A0x: x \in 'A0(S).
    have [z /setIP[Pz cyz] ntz] := trivgPn _ ntCPx. 
    apply/setUP; left; apply/bigcupP; exists z.
      by rewrite !inE ntz (subsetP (Fcore_sub_FTcore maxS)).
    by rewrite (eqP Stype2) 3!inE ntx cent1C (subsetP sUPU) ?(subsetP sR0U).
  have sCxS: 'C[x] \subset S by rewrite -['C[x]]setTI (cent1_normedTI tiA0).
  suffices <-: 'C_R[x] = R0.
    by rewrite -cent_set1 setIS ?centS // sub1set (subsetP sR0R).
  have /Hall_pi hallU: Hall PU U by rewrite -(coprime_sdprod_Hall_r defPU).
  have /Hall_pi hallPU: Hall S PU by rewrite -(coprime_sdprod_Hall_l defS).
  have sylR0_S: r.-Sylow(S) R0.
    by apply: subHall_Sylow piUr sylR0; apply: subHall_Hall (piSg sUPU) hallU.
  rewrite ['C_R[x]](sub_pHall sylR0_S) ?(pgroupS _ rR) ?subsetIl //.
    by rewrite subsetI sR0R sub_cent1 (subsetP abR0).
  by rewrite subIset ?sCxS ?orbT.
pose R1 := 'Ohm_1('Z(R))%G; pose m := logn r #|R1|.
have sR10: R1 \subset R0 by apply: gFsub_trans.
have oR1: #|R1| = (r ^ m)%N by rewrite -card_pgroup ?(pgroupS sR10).
have{sZR_R0 rR0_2} m12: pred2 1%N 2 m.
  transitivity (0 < m < 1 + 2)%N; first by rewrite -mem_iota !inE.
  rewrite -[m]p_rank_abelian ?center_abelian -?rank_pgroup ?(pgroupS sZR_R0) //.
  rewrite rank_gt0 ltnS -rR0_2 rankS // center_nil_eq1 ?(pgroup_nil rR) //.
  by rewrite (subG1_contra sR0R) // -rank_gt0 rR0_2.
have [y Qy defLy] := defL; have [_ _ /joing_subP[_ nHW2y] _] := sdprodP defLy.
have chR1H: R1 \char H.
  by rewrite !gFchar_trans // (nilpotent_Hall_pcore (Fcore_nil L) sylR) gFchar.
have nR1W2y: W2 :^ y \subset 'N(R1) by apply: char_norm_trans chR1H nHW2y.
have regR1W2y: semiregular R1 (W2 :^ y).
  have /Frobenius_reg_ker regHW12y := set_Frobenius_compl defLy frobL.
  exact: semiregularS (char_sub chR1H) (joing_subr _ _) regHW12y.
have /idPn[]: r %| p.-1./2.
  have:= piUr; rewrite mem_primes => /and3P[_ _ /=].
  by rewrite oU Euclid_dvdX ?andbT.
rewrite gtnNdvd //; first by rewrite -(subnKC pgt2).
apply: leq_trans (_ : p.-1 <= r)%N.
  by rewrite -divn2 ltn_divLR // -{1}[p.-1]muln1 -(subnKC pgt2) ltn_pmul2l.
have: p %| (r ^ m).-1.
  by have:= regular_norm_dvd_pred nR1W2y regR1W2y; rewrite cardJg oR1.
rewrite -[p.-1]subn1 leq_subLR predn_exp Euclid_dvdM // => /orP[]/dvdn_leq.
  by rewrite -(subnKC (prime_gt1 pr_r)) => /(_ isT)/leq_trans->; rewrite 2?ltnW.
case/pred2P: m12 => ->; rewrite ?(big_ord_recl 1) big_ord1 => /(_ isT) //.
by move/leq_trans->.
Qed.

(* This is Peterfalvi (14.7). *)
Let not_charUH : ~~ (U \char H).
Proof.
have [y Qy defLy] := defL; have [_ _ /joing_subP[_ nHW2y] _] := sdprodP defLy.
apply/negP=> chUH; have nUW2y := char_norm_trans chUH nHW2y.
case: no_full_FT_Galois_structure; split; last first.
  split; [by have [_ []] := FTtypeP_facts _ TtypeP | | by exists y].
  by have /sdprodP[_ _ /joing_subP[]] := Ptype_Fcore_sdprod TtypeP.
have <-: #|U| = nU.
  have regUW2y: semiregular U (W2 :^ y).
    have /Frobenius_reg_ker regHW12y := set_Frobenius_compl defLy frobL.
    exact: semiregularS (char_sub chUH) (joing_subr _ _) regHW12y.
  case: ifP (card_FTtypeP_Galois_compl maxS galS) => //.
  rewrite -/p -/q -/nU => p_modq_1 oU.
  have{p_modq_1 oU} oU: (#|U| * q)%N = nU.
    by rewrite oU divnK //; have [|_ ->] := FTtypeP_primes_mod_cases _ StypeP.
  have /eqP Umodp: #|U| == 1 %[mod p].
    have:= regular_norm_dvd_pred nUW2y regUW2y.
    by rewrite cardJg -/p -subn1 eqn_mod_dvd.
  have: nU == 1 %[mod p].
    rewrite /nU predn_exp mulKn; last by rewrite -(subnKC pgt2).
    rewrite -(ltn_predK qgt2) big_ord_recl addnC -modnDml -modn_summ modnDml.
    by rewrite big1 // => i _; rewrite expnS modnMr.
  by rewrite -oU -modnMml Umodp modnMml mul1n !modn_small ?gtn_eqF ?prime_gt1.
have [F []] := typeP_Galois_P maxS (FTtype5_exclusion maxS) galS.
rewrite Ptype_factor_prime ?(group_inj (Ptype_Fcore_kernel_trivial _ _)) //.
rewrite Ptype_Fcompl_kernel_trivial // => psiP [psiU _ [/trivgP inj_psiU psiJ]].
rewrite /= -injm_subcent ?coset1_injm ?norms1 // -morphim_comp -/p.
rewrite (typeP_cent_core_compl StypeP) => [[_ /isomP[inj_psiP im_psiP] psiW2]].
rewrite -(card_isog (quotient1_isog U)) => [[_ coUp1 _]].
suffices FPU: finFieldImage P W2 U.
  by exists FPU; have [_ []] := FTtypeP_facts maxS StypeP.
have /domP[sig [Dsig Ksig _ im_sig]]: 'dom (psiP \o coset 1) = P.
  by apply: injmK; rewrite ?coset1_injm ?norms1.
have{Ksig} inj_sig: 'injm sig by rewrite Ksig injm_comp ?coset1_injm.
exists F sig; first by apply/isomP; rewrite im_sig morphim_comp.
  by rewrite -psiW2 -im_sig injmK // -(typeP_cent_core_compl StypeP) subsetIl.
exists psiU => // z x Pz Ux /=; have inN1 x1: x1 \in 'N(1) by rewrite norm1 inE.
by rewrite !Dsig -psiJ ?mem_morphim //= qactE ?dom_qactJ.
Qed.

(* This is Peterfalvi (14.8)(a). *)
(* In order to avoid the use of real analysis and logarithms we bound the     *)
(* binomial expansion of n.+1 ^ q.+1 directly.                                *)
Let qp1_gt_pq1 : (q ^ p.+1 > p ^ q.+1)%N.
Proof.
have: (4 < p)%N by rewrite odd_geq ?mFT_odd ?(leq_trans _ ltqp).
elim: p ltqp => // n IHn; rewrite !ltnS => ngeq.
rewrite leq_eqVlt => /predU1P[/esym n4 | ngt4].
  suffices /eqP <-: 3 == q by rewrite n4.
  by rewrite eqn_leq qgt2 -ltnS -(odd_ltn 5) ?mFT_odd // -n4.
apply: leq_trans (_ : q * n ^ q.+1 <= _)%N; last first.
  rewrite (expnS q) leq_mul //.
  by move: ngeq; rewrite leq_eqVlt => /predU1P[-> | /IHn/(_ ngt4)/ltnW].
apply: leq_trans (_ : (2 * q.+1 + n) * n ^ q <= _)%N; last first.
  rewrite expnS mulnA leq_mul // addnC.
  move: ngeq; rewrite leq_eqVlt => /predU1P[-> | n_gtq].
    apply: leq_trans (_ : 4 * n <= _)%N; last by rewrite leq_mul // ltnW.
    by rewrite mulnSr addnA -mulSn (mulSnr 3) leq_add2l 3?ltnW.
  by rewrite -{2}(subnKC qgt2) addSn (mulSn _ n) leq_add2l leq_mul.
rewrite mulnDl -expnS -[n.+1]add1n expnDn big_ord_recr binn subnn !mul1n /=.
rewrite ltn_add2r -(@ltn_pmul2l (2 ^ q)) ?expn_gt0 // !mulnA -expnSr.
apply: leq_ltn_trans (_ : (2 ^ q.+1).-1 * q.+1 * n ^ q < _)%N; last first.
  by rewrite -(subnKC ngt4) !ltn_pmul2r ?prednK ?expn_gt0.
rewrite -mulnA predn_exp mul1n big_distrr big_distrl leq_sum // => [[i]] /=.
rewrite ltnS exp1n mul1n => leiq _; rewrite -{1 4}(subnKC leiq) !expnD.
rewrite -mulnA leq_mul // mulnA mulnCA mulnC leq_mul // -bin_sub ?leqW //.
rewrite -(leq_pmul2r (fact_gt0 (q.+1 - i))) -mulnA bin_ffact mulnC subSn //.
rewrite ffactnS /= -!mulnA leq_mul //=; elim: {i leiq}(q - i)%N => //= i IHi.
rewrite ffactnSr expnSr mulnACA expnS factS (mulnACA n) mulnC leq_mul //.
by rewrite leq_mul // (leq_trans (leq_subr _ _)).
Qed.

(* This is Peterfalvi (14.8)(b). *)
Let v1p_gt_u1q : (v.-1 %/ p > u.-1 %/ q)%N.
Proof.
have ub_u: (u.-1 <= nU - 1)%N.
  rewrite -subn1 leq_sub2r //; have [_ _] := FTtypeP_facts maxS StypeP.
  by rewrite (FTtypeP_reg_Fcore maxS StypeP) indexg1.
rewrite ltn_divLR ?prime_gt0 // {ub_u}(leq_ltn_trans ub_u) //.
have p_dv_v1: p %| v.-1 by have [] := FTtypeP_bridge_facts maxT TtypeP.
rewrite divn_mulAC // ltn_divRL ?dvdn_mulr // oV -subn1.
rewrite -(@ltn_pmul2l q.-1) ?(mulnCA q.-1); last by rewrite -(subnKC qgt2).
rewrite !mulnA -(@ltn_pmul2l p.-1); last by rewrite -(subnKC pgt2).
rewrite -mulnA mulnCA mulnA !(mulnBl _ _ _.-1) !divnK ?dvdn_pred_predX //.
rewrite !mul1n mulnCA -!subn1 ltn_mul ?ltn_sub2r ?prime_gt1 //.
rewrite -!subnDA !subnKC ?prime_gt0 // !mulnBl -!expnSr !mulnn.
by rewrite -subSn ?leq_exp2l ?leqW ?prime_gt1 ?leq_sub ?leq_exp2r // ltnW.
Qed.

Let calT0 := seqIndD QV T T`_\s 1.
Let rmR_T := FTtypeP_coh_base maxT TtypeP.
Let scohT0 : subcoherent calT0 tauT rmR_T.
Proof. exact: FTtypeP_subcoherent. Qed.

Let sTT0 : cfConjC_subset calS calS0.
Proof. exact/seqInd_conjC_subset1/Fcore_sub_FTcore. Qed.

(* This is Peterfalvi (14.9). *)
Lemma FTtypeP_min_typeII : FTtype T == 2.
Proof.
apply: contraLR v1p_gt_u1q => notTtype2; rewrite -leqNgt -leC_nat.
have [o_betaT0_eta _ [Ttype3 _]] := FTtype34_structure maxT TtypeP notTtype2.
have Ttype_gt2: (2 < FTtype T)%N by rewrite (eqP Ttype3).
have [[_ _ frobVW2 cVV] _ _ _ _] := FTtypeP_facts _ TtypeP.
pose calT1 := seqIndD QV T QV Q; have sT10: cfConjC_subset calT1 calT0.
  by apply/seqInd_conjC_subset1; rewrite /= FTcore_eq_der1.
rewrite (FTtypeP_reg_Fcore maxT TtypeP) (group_inj (joingG1 _)) in o_betaT0_eta.
do [rewrite -/calT1; set eta_0 := \sum_j _] in o_betaT0_eta.
have scohT1: subcoherent calT1 tauT rmR_T := subset_subcoherent scohT0 sT10.
have [nsQQV sVQV _ _ _] := sdprod_context defQV.
have nsQVT: QV <| T := der_normal 1 T.
have calT1_1p zeta: zeta \in calT1 -> zeta 1%g = p%:R.
  case/seqIndP=> s /setDP[kerQs _] -> /=; rewrite inE in kerQs.
  rewrite cfInd1 ?gFsub // -(index_sdprod defT) lin_char1 ?mulr1 //.
  rewrite lin_irr_der1 (subset_trans _ kerQs) // der1_min ?normal_norm //.
  by rewrite -(isog_abelian (sdprod_isog defQV)).
have [tau1T cohT1]: coherent calT1 T^# tauT.
  apply/(uniform_degree_coherence scohT1)/(@all_pred1_constant _ p%:R).
  by apply/allP=> _ /mapP[zeta T1zeta ->]; rewrite /= calT1_1p.
have irrT1: {subset calT1 <= irr T}.
  move=> _ /seqIndP[s /setDP[kerQs nz_s] ->]; rewrite inE in kerQs.
  rewrite inE subGcfker in nz_s; rewrite -(quo_IirrK nsQQV kerQs) mod_IirrE //.
  rewrite cfIndMod ?normal_sub ?cfMod_irr ?gFnormal //.
  rewrite irr_induced_Frobenius_ker ?quo_Iirr_eq0 //=.
  have /sdprod_isom[nQ_VW1 /isomP[injQ <-]] := Ptype_Fcore_sdprod TtypeP.
  have ->: (QV / Q)%g = (V / Q)%g by rewrite -(sdprodW defQV) quotientMidl.
  have ->: (V / Q)%g = restrm nQ_VW1 (coset Q) @* V.
    by rewrite morphim_restrm (setIidPr _) // joing_subl.
  by rewrite injm_Frobenius_ker // (FrobeniusWker frobVW2).
have [[A0betaS PVbetaS] _ [_]] := FTtypeP_bridge_facts maxS StypeP.
rewrite -/q -/u; set Gamma := FTtypeP_bridge_gap _ _ => oGa1 R_Ga lb_Ga _.
have oT1eta: orthogonal (map tau1T calT1) (map sigma (irr W)).
  apply/orthogonalP=> _ _ /mapP[zeta T1zeta ->] /mapP[omega Womega ->].
  have{omega Womega} [i [j ->]] := cycTIirrP defW Womega.
  by rewrite (cycTIisoC _ pddT) (coherent_ortho_cycTIiso _ sT10 cohT1) ?irrT1.
have [[Itau1T Ztau1T] Dtau1T] := cohT1.
have nzT1_Ga zeta: zeta \in calT1 -> `|'[Gamma, tau1T zeta]| ^+ 2 >= 1.
  have Z_Ga: Gamma \in 'Z[irr G].
    rewrite rpredD ?cycTIiso_vchar // rpredB ?rpred1 ?Dade_vchar // zchar_split.
    by rewrite A0betaS ?Iirr1_neq0 // rpredB ?cfInd_vchar ?rpred1 ?irr_vchar.
  move=> T1zeta; rewrite expr_ge1 ?normr_ge0 // norm_Cint_ge1 //.
    by rewrite Cint_cfdot_vchar ?Ztau1T ?(mem_zchar T1zeta).
  suffices: ('[Gamma, tau1T zeta] == 1 %[mod 2])%C.
    by apply: contraTneq => ->; rewrite (eqCmod_nat 2 0 1).
  pose betaT0 := nu_ 0 - zeta.
  have{o_betaT0_eta} o_eta0_betaT0 j: '[eta_ 0 j, tauT betaT0] = (j == 0)%:R.
    transitivity '[eta_ 0 j, eta_0]; rewrite (cycTIisoC _ pddT).
      apply/eqP; rewrite -subr_eq0 -cfdotBr cfdotC.
      by rewrite (orthoPl (o_betaT0_eta _ _)) ?conjC0 // map_f ?mem_irr.
    rewrite cfdot_sumr (bigD1 0) //= cfdot_cycTIiso andbT big1 ?addr0 //.
    by move=> i /negPf nz_i; rewrite cfdot_cycTIiso andbC eq_sym nz_i.
  have QVbetaT0: betaT0 \in 'CF(T, QV^#).
    rewrite cfun_onD1 rpredB ?(seqInd_on _ T1zeta) //=; last first.
      by rewrite /nu_ -cfInd_prTIres cfInd_normal.
    by rewrite !cfunE prTIred_1 prTIirr0_1 mulr1 calT1_1p ?subrr.
  have A0betaT0: betaT0 \in 'CF(T, 'A0(T)).
    by rewrite (cfun_onS (FTsupp1_sub0 _)) // /'A1(T) ?FTcore_eq_der1.
  have ZbetaT0: betaT0 \in 'Z[irr T].
    by rewrite rpredB ?char_vchar ?(seqInd_char T1zeta) ?prTIred_char.      
  pose Delta := tauT betaT0 - 1 + tau1T zeta.
  have nz_i1: #1 != 0 := Iirr1_neq0 ntW2.
  rewrite -(canLR (addKr _) (erefl Delta)) opprB cfdotDr cfdotBr oGa1 add0r.
  rewrite cfdotDl cfdotBl -/betaS o_eta0_betaT0 (negPf nz_i1) // addr0 opprB.
  rewrite -(cycTIiso1 pddS) -(cycTIirr00 defW) {}o_eta0_betaT0 mulr1n.
  have QV'betaS: tauS betaS \in 'CF(G, ~: class_support QV^# G).
    have [_ [pP _] _ _ [_ ->]] := FTtypeP_facts _ StypeP; rewrite ?A0betaS //.
    apply: cfun_onS (cfInd_on (subsetT S) (PVbetaS _ nz_i1)).
    apply/subsetP=> x PWx; rewrite inE.
    have{PWx}: p \in \pi(#[x]).
      case/imset2P: PWx => {x}x y PWx _ ->; rewrite {y}orderJ.
      case/setUP: PWx => [/setD1P[ntx Px] | /imset2P[{x}x y Wx _ ->]].
        rewrite -p_rank_gt0 -rank_pgroup ?rank_gt0 ?cycle_eq1 //.
        exact: mem_p_elt (abelem_pgroup pP) Px.
      case/setDP: Wx; rewrite {y}orderJ; have [_ <- cW12 _] := dprodP defW.
      case/mulsgP=> {x}x y W1x W2y ->; have cyx := centsP cW12 _ W2y _ W1x.
      have [-> | nty _] := eqVneq y 1%g; first by rewrite inE mulg1 W1x.
      have p'x: p^'.-elt x.
        by rewrite (mem_p_elt _ W1x) /pgroup ?pnatE ?inE ?ltn_eqF.
      have p_y: p.-elt y by rewrite (mem_p_elt (pnat_id _)).
      rewrite -cyx orderM ?(pnat_coprime p_y) // pi_ofM // inE /=.
      by rewrite -p_rank_gt0 -rank_pgroup // rank_gt0 cycle_eq1 nty.
    apply: contraL => /imset2P[z y /setD1P[_ QVz] _ ->]; rewrite {x y}orderJ.
    rewrite -p'natEpi // [_.-nat _](mem_p_elt _ QVz) // /pgroup ?p'natE //.
    rewrite -prime_coprime // coprime_sym (coprime_sdprod_Hall_r defT).
    by have [[]] := TtypeP.
  have [_ _ _ _ [_ -> //]] := FTtypeP_facts _ TtypeP.
  rewrite (cfdotElr QV'betaS (cfInd_on _ QVbetaT0)) ?subsetT //=.
  rewrite setIC setICr big_set0 mulr0 subr0 addrC /eqCmod addrK.
  rewrite cfdot_real_vchar_even ?mFT_odd ?oGa1 ?rpred0 //; split.
    rewrite rpredD ?Ztau1T ?(mem_zchar T1zeta) // rpredB ?rpred1 //.
    by rewrite Dade_vchar // zchar_split ZbetaT0.
  rewrite /cfReal -subr_eq0 opprD opprB rmorphD rmorphB rmorph1 /= addrACA.
  rewrite !addrA subrK -Dade_aut -linearB /= -/tauT rmorphB opprB /=.
  rewrite -prTIred_aut aut_Iirr0 -/nu_ [sum in tauT sum]addrC addrA subrK.
  rewrite -Dtau1T; last first.
    by rewrite (zchar_onS _ (seqInd_sub_aut_zchar _ _ _)) // setSD ?der_sub.
  rewrite raddfB -addrA addrC addrA subrK subr_eq0.
  by rewrite (cfConjC_Dade_coherent cohT1) ?mFT_odd ?irrT1.
have [Y T1_Y [X [defGa oYX oXT1]]] := orthogonal_split (map tau1T calT1) Gamma.
apply: ler_trans (lb_Ga X Y _ _ _); first 1 last; rewrite 1?addrC //.
- by rewrite cfdotC oYX conjC0.
- by apply/orthoPl=> eta Weta; rewrite (span_orthogonal oT1eta) // memv_span.
have ->: v.-1 = (p * size calT1)%N; last rewrite mulKn ?prime_gt0 //.
  rewrite [p](index_sdprod defT); have isoV := sdprod_isog defQV.
  rewrite [v](card_isog isoV) -card_Iirr_abelian -?(isog_abelian isoV) //.
  rewrite -(card_imset _ (can_inj (mod_IirrK nsQQV))) (cardD1 0) /=.
  rewrite -{1}(mod_Iirr0 QV Q) mem_imset //=.
  rewrite (size_irr_subseq_seqInd _ (subseq_refl _)) //=.
  apply: eq_card => s; rewrite !inE mem_seqInd ?gFnormal // !inE subGcfker.
  congr (_ && _); apply/idP/idP=> [/imsetP[r _ ->] | kerQs].
    by rewrite mod_IirrE ?cfker_mod.
  by rewrite -(quo_IirrK nsQQV kerQs) mem_imset.
have o1T1: orthonormal (map tau1T calT1).
  rewrite map_orthonormal ?(sub_orthonormal irrT1) ?seqInd_uniq //.
  exact: irr_orthonormal.
have [_ -> ->] := orthonormal_span o1T1 T1_Y.
rewrite cfnorm_sum_orthonormal // big_map -sum1_size natr_sum !big_seq.
apply: ler_sum => // zeta T1zeta; rewrite -(canLR (addrK X) defGa).
by rewrite cfdotBl (orthoPl oXT1) ?subr0 ?nzT1_Ga ?map_f.
Qed.
Let Ttype2 := FTtypeP_min_typeII.

(* These declarations correspond to Hypothesis (14.10). *)
Variables (M : {group gT}) (tau1M : {additive 'CF(M) -> 'CF(G)}) (psi : 'CF(M)).
Hypothesis maxNV_M : M \in 'M('N(V)).

Local Notation "` 'M'" := (gval M) (at level 0, only parsing).
Local Notation K := `M`_\F%G.
Local Notation "` 'K'" := `M`_\F%g (at level 0, format "` 'K'") : group_scope.

(* Consequences of the above. *)
Hypotheses (maxM : M \in 'M) (sNVM : 'N(V) \subset M).
Hypotheses (frobM : [Frobenius M with kernel K]) (Mtype1 : FTtype M == 1%N).

Let calM := seqIndD K M K 1.
Local Notation tauM := (FT_DadeF maxM).
Let nsKM : K <| M. Proof. exact: gFnormal. Qed.
Let irrM : {subset calM <= irr M}. Proof. exact: FTtype1_Ind_irr. Qed.

Hypothesis cohM : coherent_with calM M^# tauM tau1M.
Hypotheses (Mpsi : psi \in calM) (psi1 : psi 1%g = #|M : K|%:R).

Let betaM := 'Ind[M, K] 1 - psi.

Let pairTS : typeP_pair T S xdefW. Proof. exact: typeP_pair_sym pairST. Qed.

Let pq : algC := (p * q)%:R.
Let h := #|H|.

(* This is the first (and main) part of Peterfalvi (14.11). *)
Let defK : `K = V.
Proof.
pose e := #|M : K|; pose k := #|K|; apply: contraTeq isT => notKV.
have [_ sVK defM] := FTtypeII_support_facts maxT TtypeP Ttype2 pairTS maxNV_M.
have ltVK: V \proper K by rewrite properEneq eq_sym notKV.
have e_dv_k1: e %| k.-1 := Frobenius_ker_dvd_ker1 frobM.
have [e_lepq regKW2]: (e <= p * q)%N /\ semiregular K W2.
  case: defM => [|[y Py]] defM; rewrite /e -(index_sdprod defM).
    have /Frobenius_reg_ker regHW1 := set_Frobenius_compl defM frobM.
    by rewrite leq_pmulr ?cardG_gt0.
  have /Frobenius_reg_ker regHW21y := set_Frobenius_compl defM frobM.
  split; last exact: semiregularS (joing_subl _ _) regHW21y.
  suffices /normP <-: y \in 'N(W2).
    by rewrite -conjYg cardJg (dprodWY xdefW) -(dprod_card xdefW).
  have cPP: abelian P by have [_ [/and3P[]]] := FTtypeP_facts maxS StypeP.
  have sW2P: W2 \subset P by have [_ _ _ []] := StypeP.
  by rewrite (subsetP _ y Py) // sub_abelian_norm.
(* This is (14.11.1). *)
have{regKW2} [lb_k lb_k1e_v]: (2 * p * v < k /\ v.-1 %/ p < k.-1 %/ e)%N.
  have /dvdnP[x Dk]: v %| k := cardSg sVK.
  have lb_x: (p.*2 < x)%N.
    have x_gt1: (1 < x)%N.
      by rewrite -(ltn_pmul2r (cardG_gt0 V)) -Dk mul1n proper_card.
    have x_gt0 := ltnW x_gt1; rewrite -(prednK x_gt0) ltnS -subn1.
    rewrite dvdn_leq ?subn_gt0 // -mul2n Gauss_dvd ?coprime2n ?mFT_odd //.
    rewrite dvdn2 odd_sub // (dvdn_odd _ (mFT_odd K)) -/k ?Dk ?dvdn_mulr //=.
    rewrite -eqn_mod_dvd // -[x]muln1 -modnMmr.
    have nVW2: W2 \subset 'N(V) by have [_ []] := TtypeP.
    have /eqP{1} <-: (v == 1 %[mod p]).
      rewrite eqn_mod_dvd ?cardG_gt0 // subn1 regular_norm_dvd_pred //.
      exact: semiregularS regKW2.
    rewrite modnMmr -Dk /k eqn_mod_dvd // subn1 regular_norm_dvd_pred //.
    by rewrite (subset_trans (subset_trans nVW2 sNVM)) ?gFnorm.
  have lb_k: (2 * p * v < k)%N by rewrite mul2n Dk ltn_pmul2r ?cardG_gt0.
  split=> //; rewrite ltn_divLR ?cardG_gt0 // divn_mulAC ?prednK ?cardG_gt0 //.
  rewrite leq_divRL ?indexg_gt0 // (leq_trans (leq_mul (leqnn v) e_lepq)) //.
  rewrite mulnA mulnAC leq_mul // -ltnS prednK ?cardG_gt0 //.
  apply: leq_ltn_trans lb_k; rewrite mulnC leq_mul // ltnW ?(leq_trans ltqp) //.
  by rewrite mul2n -addnn leq_addl.
have lb_k1e_u := ltn_trans v1p_gt_u1q lb_k1e_v; have irr_psi := irrM Mpsi.
have Mgt1: (1 < size calM)%N by apply: seqInd_nontrivial Mpsi; rewrite ?mFT_odd.
(* This is (14.11.2). *)
have [] // := FTtype2_support_coherence TtypeP StypeP cohM Mpsi.
rewrite -/e -/p -/q mulnC /= => De [nb [chi Dchi]].
rewrite cycTIiso_irrelC -/sigma -/betaM => DbetaM.
pose ddMK := FT_DadeF_hyp maxM; pose AM := Dade_support ddMK.
have defAM: AM = 'A~(M) by rewrite FTsupp_Frobenius -?FT_DadeF_supportE.
pose ccG A := class_support A G.
pose G0 := ~: ('A~(M) :|: ccG What :|: ccG P^# :|: ccG Q^#).
have sW2P: W2 \subset P by have [_ _ _ []] := StypeP.
have sW1Q: W1 \subset Q by have [_ _ _ []] := TtypeP.
(* This is (14.11.3). *)
have lbG0 g: g \in G0 -> 1 <= `|tau1M psi g| ^+ 2.
  rewrite !inE ?expr_ge1 ?normr_ge0 // => /norP[/norP[/norP[AM'g W'g P'g Q'g]]].
  have{W'g} /coprime_typeP_Galois_core-co_p_g: g \notin ccG W^#.
    apply: contra W'g => /imset2P[x y /setD1P[ntx Wx] Gy Dg].
    rewrite Dg mem_imset2 // !inE Wx andbT; apply/norP; split.
      by apply: contra Q'g => /(subsetP sW1Q)?; rewrite Dg mem_imset2 ?inE ?ntx.
    by apply: contra P'g => /(subsetP sW2P)Px; rewrite Dg mem_imset2 ?inE ?ntx.
  have{AM'g} betaMg0: tauM betaM g = 0.
    by apply: cfun_on0 AM'g; rewrite -defAM Dade_cfunS.
  suffices{betaMg0}: 1 <= `|(\sum_ij (-1) ^+ nb ij *: sigma 'chi_ij) g|.
    rewrite -[\sum_i _](subrK chi) -DbetaM !cfunE betaMg0 add0r.
    case: Dchi => -> //; rewrite cfunE normrN.
    by rewrite -(cfConjC_Dade_coherent cohM) ?mFT_odd ?cfunE ?norm_conjC.
  have{co_p_g} Zeta_g ij: sigma 'chi_ij g \in Cint.
    apply/Cint_cycTIiso_coprime/(coprime_dvdr (cforder_lin_char_dvdG _)).
      by apply: irr_cyclic_lin; have [] := ctiWG.
    rewrite -(dprod_card defW) coprime_mulr.
    by apply/andP; split; [apply: co_p_g galT _ | apply: co_p_g galS _].
  rewrite sum_cfunE norm_Cint_ge1 ?rpred_sum // => [ij _|].
    by rewrite cfunE rpredMsign.
  set a := \sum_i _; suffices: (a == 1 %[mod 2])%C.
    by apply: contraTneq=> ->; rewrite (eqCmod_nat 2 0 1).
  have signCmod2 n ij (b := sigma 'chi_ij g): ((-1) ^+ n * b == b %[mod 2])%C.
    rewrite -signr_odd mulr_sign eqCmod_sym; case: ifP => // _.
    by rewrite -(eqCmodDl _ b) subrr -[b + b](mulr_natr b 2) eqCmodMl0 /b.
  rewrite -[1]addr0 [a](bigD1 0) {a}//= cfunE eqCmodD //.
    by rewrite (eqCmod_trans (signCmod2 _ _)) // irr0 cycTIiso1 cfun1E inE.
  rewrite (partition_big_imset (fun ij => [set ij; conjC_Iirr ij])) /= eqCmod0.
  apply: rpred_sum => _ /=/imsetP[ij /negPf nz_ij ->].
  rewrite (bigD1 ij) /=; last by rewrite unfold_in nz_ij eqxx.
  rewrite (big_pred1 (conjC_Iirr ij)) => [|ij1 /=]; last first.
    rewrite unfold_in eqEsubset !subUset !sub1set !inE !(eq_sym ij).
    rewrite !(can_eq (@conjC_IirrK _ _)) (canF_eq (@conjC_IirrK _ _)).
    rewrite -!(eq_sym ij1) -!(orbC (_ == ij)) !andbb andbAC -andbA.
    rewrite andb_orr andNb andbA andb_idl // => /eqP-> {ij1}.
    rewrite conjC_Iirr_eq0 nz_ij -(inj_eq irr_inj) conjC_IirrE.
    by rewrite odd_eq_conj_irr1 ?mFT_odd // irr_eq1 nz_ij.
  rewrite -signr_odd -[odd _]negbK signrN !cfunE mulNr addrC.
  apply: eqCmod_trans (signCmod2 _ _) _.
  by rewrite eqCmod_sym conjC_IirrE -cfAut_cycTIiso cfunE conj_Cint.
have cardG_D1 R: #|R^#| = #|R|.-1 by rewrite [#|R|](cardsD1 1%g) group1.
pose rho := invDade ddMK; pose nG : algC := #|G|%:R.
pose sumG0 := \sum_(g in G0) `|tau1M psi g| ^+ 2.
pose sumG0_diff := sumG0 - (#|G0| + #|ccG What| + #|ccG P^#| + #|ccG Q^#|)%:R.
have ub_rho: '[rho (tau1M psi)] <= k.-1%:R / #|M|%:R - nG^-1 * sumG0_diff.
  have NtauMpsi: '[tau1M psi] = 1.
    by have [[Itau1 _] _] := cohM; rewrite Itau1 ?mem_zchar //= irrWnorm.
  rewrite ler_subr_addl -subr_le0 -addrA.
  have ddM_ i j: i != j :> 'I_1 -> [disjoint AM & AM] by rewrite !ord1.
  apply: ler_trans (Dade_cover_inequality ddM_ NtauMpsi); rewrite -/nG -/AM.
  rewrite !big_ord1 cardG_D1 ler_add2r ler_pmul2l ?invr_gt0 ?gt0CG //= defAM.
  rewrite setTD ler_add ?ler_opp2 ?leC_nat //; last first.
    do 3!rewrite -?addnA -cardsUI ?addnA (leq_trans _ (leq_addr _ _)) //.
    by rewrite subset_leq_card // -setCD setCS -!setUA subDset setUC.
  rewrite (big_setID G0) /= (setIidPr _) ?setCS -?setUA ?subsetUl // ler_addl.
  by apply: sumr_ge0 => g _; rewrite ?exprn_ge0 ?normr_ge0.
have lb_rho: 1 - pq / k%:R <= '[rho (tau1M psi)].
  have [_] := Dade_Ind1_sub_lin cohM Mgt1 irr_psi Mpsi psi1; rewrite -/e -/k.
  rewrite odd_Frobenius_index_ler ?mFT_odd // => -[_ _ [|/(ler_trans _)->] //].
  by rewrite ler_add2l ler_opp2 ler_pmul2r ?invr_gt0 ?gt0CG // leC_nat.
have{rho sumG0 sumG0_diff ub_rho lb_rho} []:
  ~ pq / k%:R + 2%:R / pq + (u * q)%:R^-1 + (v * p)%:R^-1 < p%:R^-1 + q%:R^-1.
- rewrite ler_gtF // -!addrA -ler_subl_addl -ler_subr_addl -(ler_add2l 1).
  apply: ler_trans {ub_rho lb_rho}(ler_trans lb_rho ub_rho) _.
  rewrite /sumG0_diff -!addnA natrD opprD addrA mulrBr opprB addrA.
  rewrite ler_subl_addr ler_paddr //.
    by rewrite mulr_ge0 ?invr_ge0 ?ler0n // subr_ge0 -sumr_const ler_sum.
  rewrite mulrDl -!addrA addrCA [1 + _]addrA [_ + (_ - _)]addrA ler_add //.
    rewrite -(Lagrange (normal_sub nsKM)) natrM invfM mulrA -/k -/e /pq -De.
    rewrite ler_pmul2r ?invr_gt0 ?gt0CiG // ler_pdivr_mulr ?gt0CG //.
    by rewrite mul1r leC_nat leq_pred.
  rewrite [1 + _ + _]addrA addrAC !natrD !mulrDr !ler_add //; first 1 last.
  + exact: (FTtype2_cc_core_ler StypeP).
  + exact: (FTtype2_cc_core_ler TtypeP).
  have [_ _ /card_support_normedTI->] := ctiWG.
  rewrite natrM natf_indexg ?subsetT // mulrCA mulKf ?neq0CG // card_cycTIset.
  rewrite mulnC -(dprod_card xdefW) /pq !natrM -!subn1 !natrB // -/p -/q invfM.
  rewrite mulrACA !mulrBl ?divff ?neq0CG // !mul1r mulrBr mulr1 opprB.
  by rewrite addrACA -opprB opprK.
rewrite -!addrA ler_lt_add //; last first.
  pose q2 : algC := (q ^ 2)%:R.
  apply: ltr_le_trans (_ : 2%:R / q2 + (2%:R * q2)^-1 *+ 2 <= _); last first.
    rewrite addrC -[_ *+ 2]mulr_natl invfM mulVKf ?pnatr_eq0 //.
    rewrite mulr_natl -mulrS -mulr_natl [q2]natrM.
    by rewrite ler_pdivr_mulr ?mulr_gt0 ?gt0CG // mulKf ?neq0CG ?leC_nat.
  rewrite -natrM !addrA ltr_add ?(FTtypeP_complV_ltr TtypeP) 1?ltnW //.
  rewrite ltr_add ?(FTtypeP_complV_ltr StypeP) // /pq mulnC /q2 !natrM !invfM.
  by rewrite !ltr_pmul2l ?ltf_pinv ?invr_gt0 ?qualifE ?gt0CG ?ltr0n ?ltr_nat.
rewrite ler_pdivr_mulr ?ler_pdivl_mull ?gt0CG // -natrM leC_nat.
apply: leq_trans lb_k; rewrite leqW // mulnAC mulnC leq_mul //.
have [[_ _ frobVW2 _] _ _ _ _] := FTtypeP_facts maxT TtypeP.
rewrite -[(p * q)%N]mul1n leq_mul // (leq_trans _ (leq_pred v)) // dvdn_leq //.
  by rewrite -subn1 subn_gt0 cardG_gt1; have[] := Frobenius_context frobVW2.
rewrite Gauss_dvd ?prime_coprime ?(dvdn_prime2 pr_p pr_q) ?gtn_eqF //.
rewrite (Frobenius_dvd_ker1 frobVW2) /= oV /nV predn_exp.
rewrite -(subnKC qgt2) -(ltn_predK pgt2) mulKn // subnKC //.
by rewrite big_ord_recl dvdn_sum // => i _; rewrite expnS dvdn_mulr.
Qed.

(* This is the first part of Peterfalvi (14.11). *)
Let indexMK : #|M : K| = (p * q)%N.
Proof.
have [_ _ [defM|]] := FTtypeII_support_facts maxT TtypeP Ttype2 pairTS maxNV_M.
  have:= Ttype2; rewrite (mmax_max maxM (mmax_proper maxT)) ?(eqP Mtype1) //.
  rewrite -(sdprodW (Ptype_Fcore_sdprod TtypeP)) -defK (sdprodWY defM).
  exact: mulG_subr.
case=> y Py /index_sdprod <-; rewrite (dprod_card xdefW) -(dprodWY xdefW).
suffices /normP {1}<-: y \in 'N(W2) by rewrite -conjYg cardJg.
have cPP: abelian P by have [_ [/and3P[]]] := FTtypeP_facts maxS StypeP.
by rewrite (subsetP (sub_abelian_norm cPP _)) //; have [_ _ _ []] := StypeP.
Qed.

(* This is Peterfalvi (14.12), and also (14.13) since we have already proved  *)
(* the negation of Theorem (14.2).                                            *)
Let not_MG_L : (L : {set gT}) \notin M :^: G.
Proof.
rewrite orbit_sym; apply: contra not_charUH => /imsetP[z _ /= defLz].
rewrite sub_cyclic_char // -(cyclicJ _ z) -FcoreJ -defLz defK.
have [_ _ [cycV _ _]] := typeP_Galois_P maxT (FTtype5_exclusion maxT) galT.
rewrite Ptype_Fcompl_kernel_trivial // in cycV.
by rewrite -(isog_cyclic (quotient1_isog V)) in cycV.
Qed.

(* This is Peterfalvi (14.14). *)
Let LM_cases :
    '[tauM betaM, tau1L phi] != 0 /\ h.-1%:R / pq <= pq - 1
 \/ '[tauL betaL, tau1M psi] != 0 /\ q = 3 /\ p = 5.
Proof.
have [irr_phi irr_psi] := (irrL Lphi, irrM Mpsi).
have:= Dade_sub_lin_nonorthogonal (mFT_odd _) _ cohM cohL _ Mpsi _ _ Lphi.
rewrite -/betaL -/betaM disjoint_Dade_FTtype1 //.
case=> //; set a := '[_, _] => nz_a; [left | right]; split=> //.
  rewrite {1}/pq -indexLH /pq -indexMK.
  by rewrite (coherent_FTtype1_core_ltr cohM cohL Mpsi Lphi) // orbit_sym.
have ub_v: v.-1%:R / pq <= pq - 1.
  rewrite {1}/pq -indexMK /pq -indexLH /v -defK.
  exact: (coherent_FTtype1_core_ltr cohL cohM Lphi Mpsi).
have{ub_v} ub_qp: (q ^ (p - 3) < p ^ 2)%N.
  rewrite -(@ltn_pmul2l (q ^ 3)) ?expn_gt0 ?cardG_gt0 // -expnD subnKC //.
  have: v.-1%:R < pq ^+ 2.
    rewrite -ltr_pdivr_mulr ?ltr0n ?muln_gt0 ?cardG_gt0 //.
    by rewrite (ler_lt_trans ub_v) // ltr_subl_addl -mulrS ltC_nat.
  rewrite -natrX ltC_nat prednK ?cardG_gt0 // mulnC expnMn oV.
  rewrite leq_divLR ?dvdn_pred_predX // mulnC -subn1 leq_subLR.
  move/leq_ltn_trans->; rewrite // -addSn addnC -(leq_add2r (q ^ 2 * p ^ 2)).
  rewrite addnAC -mulSnr prednK ?cardG_gt0 // mulnA leq_add2l -expnMn.
  by rewrite (ltn_sqr 1) (@ltn_mul 1 1) ?prime_gt1.
have q3: q = 3.
  apply/eqP; rewrite eqn_leq qgt2 -ltnS -(odd_ltn 5) ?mFT_odd // -ltnS.
  rewrite -(ltn_exp2l _ _ (ltnW pgt2)) (leq_trans qp1_gt_pq1) // ltnW //.
  by rewrite -{1}(subnK pgt2) -addnS expnD (expnD p 2 4) ltn_mul ?ltn_exp2r.
split=> //; apply/eqP; rewrite eqn_leq -ltnS andbC.
rewrite (odd_geq 5) -1?(odd_ltn 7) ?mFT_odd //= doubleS -{1}q3 ltqp /=.
move: ub_qp; rewrite 2!ltnNge q3; apply: contra.
elim: p => // x IHx; rewrite ltnS leq_eqVlt => /predU1P[<- // | xgt6].
apply: (@leq_trans (3 * x ^ 2)); last first.
  rewrite subSn ?(leq_trans _ xgt6) //.
  by rewrite [rhs in (_ <= rhs)%N]expnS leq_mul ?IHx.
rewrite -addn1 sqrnD -addnA (mulSn 2) leq_add2l muln1.
rewrite (@leq_trans (2 * (x * 7))) ?leq_mul //.
by rewrite mulnCA (mulnDr x 12 2) mulnC leq_add2r -(subnKC xgt6).
Qed.

(* This is Peterfalvi (14.15). *)
Let oU : u = nU.
Proof.
case: ifP (card_FTtypeP_Galois_compl maxS galS) => // p1modq oU.
pose x := #|H : U|; rewrite -/u -/nU -/p -/q in p1modq oU.
have DnU: (q * u)%N = nU.
  rewrite mulnC oU divnK //.
  by have [_ ->] := FTtypeP_primes_mod_cases maxS StypeP.
have oH: h = (u * x)%N by rewrite Lagrange.
have xmodp: x = q %[mod p].
  have hmodp: h = 1 %[mod p].
    apply/eqP; rewrite eqn_mod_dvd ?cardG_gt0 // subn1.
    apply: dvdn_trans (Frobenius_ker_dvd_ker1 frobL).
    have [y _ /index_sdprod <-] := defL.
    by rewrite -[p](cardJg _ y) cardSg ?joing_subr.
  rewrite -[q]muln1 -modnMmr -hmodp modnMmr oH mulnA DnU -modnMml.
  suffices ->: nU = 1 %[mod p] by rewrite modnMml mul1n.
  rewrite /nU predn_exp mulKn; last by rewrite -(subnKC pgt2).
  apply/eqP; rewrite -(ltn_predK qgt2) big_ord_recl eqn_mod_dvd ?subn1 //=.
  by apply: dvdn_sum => i _; rewrite expnS dvdn_mulr.
have{xmodp} [n Dx]: {n | x = q + n * p}%N.
  by exists (x %/ p); rewrite -(modn_small ltqp) addnC -xmodp -divn_eq.
have nmodq: n = 1 %[mod q].
  have [y _ defLy] := defL; have [_ _ /joing_subP[nHW1 _] _] := sdprodP defLy.
  have regHW1: semiregular H W1.
    have /Frobenius_reg_ker := set_Frobenius_compl defLy frobL.
    by apply: semiregularS; rewrite ?joing_subl.
  have hmodq: h = 1 %[mod q].
    apply/eqP; rewrite eqn_mod_dvd ?cardG_gt0 // subn1.
    exact: regular_norm_dvd_pred regHW1.
  have umodq: u = 1 %[mod q].
    apply/eqP; rewrite eqn_mod_dvd ?cardG_gt0 // subn1.
    apply: regular_norm_dvd_pred; first by have [_ []] := StypeP.
    exact: semiregularS regHW1.
  rewrite -hmodq oH -modnMml umodq modnMml mul1n Dx modnDl.
  by rewrite -modnMmr (eqP p1modq) modnMmr muln1.
have{n nmodq Dx} lb_x: (q + q.+1 * p <= x)%N.
  rewrite (divn_eq n q) nmodq (modn_small (ltnW qgt2)) addn1 in Dx.
  rewrite Dx leq_add2l leq_mul // ltnS leq_pmull // lt0n.
  have: odd x by rewrite (dvdn_odd (dvdn_indexg _ _)) ?mFT_odd.
  by rewrite Dx odd_add odd_mul !mFT_odd; apply: contraNneq => ->.
have lb_h: (p ^ q < h)%N.
  rewrite (@leq_trans (p * nU)) //; last first.
    rewrite -DnU oH mulnA mulnC leq_mul // (leq_trans _ lb_x) //.
    by rewrite mulSn addnA mulnC leq_addl.
  rewrite /nU predn_exp mulKn; last by rewrite -(subnKC pgt2).
  rewrite -(subnKC (ltnW qgt2)) subn2 big_ord_recr big_ord_recl /=.
  by rewrite -add1n !mulnDr -!expnS -addnA leq_add ?leq_addl // cardG_gt0.
have ub_h: (h <= p ^ 2 * q ^ 2)%N.
  have [[_ ub_h] | [_ [q3 p5]]] := LM_cases; last by rewrite q3 p5 in p1modq.
  rewrite -expnMn -(ltn_predK lb_h) -ltC_nat natrM -/pq.
  rewrite -ltr_pdivr_mulr ?ltr0n ?muln_gt0 ?cardG_gt0 //.
  by rewrite (ler_lt_trans ub_h) // ltr_subl_addl -mulrS ltC_nat.
have{lb_h} lb_q2: (p ^ q.-2 < q ^ 2)%N.
  rewrite -(@ltn_pmul2l (p ^ 2)) ?expn_gt0 ?cardG_gt0 // (leq_trans _ ub_h) //.
  by rewrite -subn2 -expnD subnKC // ltnW.
have q3: q = 3.
  apply/eqP; rewrite eqn_leq qgt2 -(subnKC (ltnW qgt2)) subn2 ltnS.
  by rewrite -(ltn_exp2l _ _ (ltnW pgt2)) (ltn_trans lb_q2) ?ltn_exp2r.
have{lb_q2 p1modq} p7: p = 7.
  suff: p \in [seq n <- iota 4 5 | prime n & n == 1 %[mod 3]] by case/predU1P.
  by rewrite mem_filter pr_p mem_iota -q3 p1modq ltqp; rewrite q3 in lb_q2 *.
rewrite oH mulnC oU /nU q3 p7 -leq_divRL //= in ub_h lb_x.
by have:= leq_trans lb_x ub_h.
Qed.

(* This is Peterfalvi (14.16), the last step towards the final contradiction. *)
Let defH : `H = U.
Proof.
pose x := #|H : U|; have oH: h = (u * x)%N by rewrite Lagrange.
apply/eqP/idPn; rewrite eqEsubset sUH andbT -indexg_gt1 -/x => xgt1.
have hmodpq: h = 1 %[mod p * q].
  apply/eqP; rewrite eqn_mod_dvd ?cardG_gt0 // -indexLH subn1.
  exact: Frobenius_ker_dvd_ker1.
have [[_ _ frobUW1 _] _ _ _ _] := FTtypeP_facts maxS StypeP.
have /eqP umodpq: u == 1 %[mod p * q].
  rewrite chinese_remainder ?prime_coprime ?dvdn_prime2 ?(gtn_eqF ltqp) //.
  rewrite !eqn_mod_dvd ?cardG_gt0 // subn1 (Frobenius_dvd_ker1 frobUW1).
  rewrite oU /nU predn_exp mulKn; last by rewrite -(subnKC pgt2).
  by rewrite -(ltn_predK qgt2) big_ord_recl dvdn_sum //= => i; rewrite dvdn_exp.
have{hmodpq} lb_x: (p * q < x)%N.
  rewrite -(subnKC (ltnW xgt1)) ltnS dvdn_leq ?subn_gt0 //.
  by rewrite -eqn_mod_dvd 1?ltnW // -hmodpq oH -modnMml umodpq modnMml mul1n.
have [[_ ub_h] | [nz_a [q3 p5]]] := LM_cases.
  have /idPn[]: (p * q < u)%N.
    have ugt1: (1 < u)%N.
      by rewrite cardG_gt1; have [] := Frobenius_context frobUW1.
    rewrite -(subnKC (ltnW ugt1)) ltnS dvdn_leq ?subn_gt0 //.
    by rewrite -eqn_mod_dvd ?umodpq 1?ltnW.
  rewrite -leqNgt -(leq_pmul2r (indexg_gt0 L H)) indexLH.
  apply: (@leq_trans h.-1).
    by rewrite -ltnS prednK ?cardG_gt0 // oH ltn_pmul2l ?cardG_gt0.
  rewrite -indexLH -leC_nat natrM -ler_pdivr_mulr ?gt0CiG // indexLH -/pq.
  by rewrite (ler_trans ub_h) // ler_subl_addl -mulrS leC_nat ltnW.
have lb_h1e_v: (v.-1 %/ p < h.-1 %/ #|L : H|)%N.
  rewrite -(@ltn_pmul2l u) ?cardG_gt0 // -oH oU /nU q3 p5 /= in lb_x.
  rewrite -(ltn_subRL 1) /= subn1 in lb_x.
  by rewrite leq_divRL ?indexG_gt0 // oV /nV indexLH q3 p5 (leq_trans _ lb_x).
have oLM: orthogonal (map tau1L calL) (map tau1M calM).
  by rewrite orthogonal_sym coherent_FTtype1_ortho.
case/eqP: nz_a; have lb_h1e_u := ltn_trans v1p_gt_u1q lb_h1e_v.
have [] // := FTtype2_support_coherence StypeP TtypeP cohL Lphi.
rewrite -/tauL -/sigma => _ [nb [chi Dchi ->]].
rewrite cfdotBl cfdot_suml big1 => [|ij _]; last first.
  have [_ o_tauMeta _ _] := FTtypeI_bridge_facts _ StypeP Mtype1 cohM Mpsi psi1.
  rewrite cfdotZl cfdotC (orthogonalP o_tauMeta) ?map_f ?mem_irr //.
  by rewrite conjC0 mulr0.
case: Dchi => ->; first by rewrite (orthogonalP oLM) ?map_f // subr0.
by rewrite cfdotNl opprK add0r (orthogonalP oLM) ?map_f // cfAut_seqInd.
Qed.

Lemma FTtype2_exclusion : False.
Proof. by have /negP[] := not_charUH; rewrite /= defH char_refl. Qed.

End Fourteen.

Lemma no_minSimple_odd_group (gT : minSimpleOddGroupType) : False.
Proof.
have [/forall_inP | [S [T [_ W W1 W2 defW pairST]]]] := FTtypeP_pair_cases gT.
  exact/negP/not_all_FTtype1.
have xdefW: W2 \x W1 = W by rewrite dprodC.
have pairTS := typeP_pair_sym xdefW pairST.
pose p := #|W2|; pose q := #|W1|.
have p'q: q != p.
  have [[[ctiW _ _] _ _ _ _] /mulG_sub[sW1W sW2W]] := (pairST, dprodW defW).
  have [cycW _ _] := ctiW; apply: contraTneq (cycW) => eq_pq.
  rewrite (cyclic_dprod defW) ?(cyclicS _ cycW) // -/q eq_pq.
  by rewrite /coprime gcdnn -trivg_card1; have [] := cycTI_nontrivial ctiW.
without loss{p'q} ltqp: S T W1 W2 defW xdefW pairST pairTS @p @q / q < p.
  move=> IH_ST; rewrite neq_ltn in p'q.
  by case/orP: p'q; [apply: (IH_ST S T) | apply: (IH_ST T S)].
have [[_ maxS maxT] _ _ _ _] := pairST.
have [[U StypeP] [V TtypeP]] := (typeP_pairW pairST, typeP_pairW pairTS).
have Stype2: FTtype S == 2 := FTtypeP_max_typeII maxS StypeP ltqp.
have Ttype2: FTtype T == 2 := FTtypeP_min_typeII maxS maxT StypeP TtypeP ltqp.
have /mmax_exists[L maxNU_L]: 'N(U) \proper setT.
  have [[_ ntU _ _] cUU _ _ _] := compl_of_typeII maxS StypeP Stype2.
  by rewrite mFT_norm_proper // mFT_sol_proper abelian_sol.
have /mmax_exists[M maxNV_M]: 'N(V) \proper setT.
  have [[_ ntV _ _] cVV _ _ _] := compl_of_typeII maxT TtypeP Ttype2.
  by rewrite mFT_norm_proper // mFT_sol_proper abelian_sol.
have [[maxL sNU_L] [maxM sNV_M]] := (setIdP maxNU_L, setIdP maxNV_M).
have [frobL sUH _] := FTtypeII_support_facts maxS StypeP Stype2 pairST maxNU_L.
have [frobM _ _] := FTtypeII_support_facts maxT TtypeP Ttype2 pairTS maxNV_M.
have Ltype1 := FT_Frobenius_type1 maxL frobL.
have Mtype1 := FT_Frobenius_type1 maxM frobM.
have [tau1L cohL] := FTtype1_coherence maxL Ltype1.
have [tau1M cohM] := FTtype1_coherence maxM Mtype1.
have [phi Lphi phi1] := FTtype1_ref_irr maxL.
have [psi Mpsi psi1] := FTtype1_ref_irr maxM.
exact: (FTtype2_exclusion pairST maxS maxT StypeP TtypeP ltqp
                          maxNU_L sNU_L sUH frobL Ltype1 cohL Lphi phi1
                          maxNV_M sNV_M frobM Mtype1 cohM Mpsi psi1).
Qed.

Theorem Feit_Thompson (gT : finGroupType) (G : {group gT}) :
  odd #|G| -> solvable G.
Proof. exact: (minSimpleOdd_ind no_minSimple_odd_group). Qed.

Theorem simple_odd_group_prime (gT : finGroupType) (G : {group gT}) :
  odd #|G| -> simple G -> prime #|G|.
Proof. exact: (minSimpleOdd_prime no_minSimple_odd_group). Qed.