move odd_order to its own repository

1 files changed, 0 insertions, 1203 deletions

diff --git a/mathcomp/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v
deleted file mode 100644
index 3635618..0000000
--- a/mathcomp/odd_order/PFsection11.v
+++ /dev/null
@@ -1,1203 +0,0 @@
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly finset center.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
-From mathcomp
-Require Import gfunctor gproduct cyclic commutator gseries nilpotent pgroup.
-From mathcomp
-Require Import sylow hall abelian maximal frobenius.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation mxabelem vector.
-From mathcomp
-Require Import BGsection1 BGsection3 BGsection7 BGsection15 BGsection16.
-From mathcomp
-Require Import ssrnum ssrint algC classfun character inertia vcharacter.
-From mathcomp
-Require Import PFsection1 PFsection2 PFsection3 PFsection4 PFsection5.
-From mathcomp
-Require Import PFsection6 PFsection7 PFsection8 PFsection9 PFsection10.
-
-(******************************************************************************)
-(* This file covers Peterfalvi, Section 11: Maximal subgroups of Types        *)
-(* III and IV.                                                                *)
-(******************************************************************************)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Import GroupScope GRing.Theory FinRing.Theory Num.Theory.
-
-Section Eleven.
-
-(* This is Peterfalvi (11.1). *)
-Lemma lbound_expn_odd_prime p q : 
-   odd p -> odd q -> prime p -> prime q -> p != q -> 4 * q ^ 2 + 1 < p ^ q.
-Proof.
-move=> odd_p odd_q pr_p pr_q p_neq_q.
-have{pr_p pr_q} [pgt2 qgt2] : 2 < p /\ 2 < q by rewrite !odd_prime_gt2.
-have [qlt5 | qge5 {odd_q qgt2 p_neq_q}] := ltnP q 5.
-  have /eqP q3: q == 3 by rewrite eqn_leq qgt2 andbT -ltnS -(odd_ltn 5).
-  apply: leq_trans (_ : 5 ^ q <= p ^ q); first by rewrite q3.
-  by rewrite leq_exp2r // odd_geq // ltn_neqAle pgt2 eq_sym -q3 p_neq_q.
-apply: leq_trans (_ : 3 ^ q <= p ^ q); last by rewrite -(subnKC qge5) leq_exp2r.
-elim: q qge5 => // q IHq; rewrite ltnS leq_eqVlt => /predU1P[<- // | qge5].
-rewrite (expnS 3); apply: leq_trans {IHq}(leq_mul (leqnn 3) (IHq qge5)).
-rewrite -!addnS mulnDr leq_add // mulnCA leq_mul // !(mul1n, mulSnr).
-by rewrite -addn1 sqrnD muln1 -(subnKC qge5) !leq_add ?leq_mul.
-Qed.
-
-Local Open Scope ring_scope.
-
-Variable gT : minSimpleOddGroupType.
-Local Notation G := (TheMinSimpleOddGroup gT).
-Implicit Types H K L N P Q R S T U V W : {group gT}.
-
-Variables M U W W1 W2 : {group gT}.
-Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W) (MtypeP : of_typeP M U defW).
-Hypothesis notMtype2 : FTtype M != 2.
-
-Let notMtype5 : FTtype M != 5. Proof. exact: FTtype5_exclusion. Qed.
-Let notMtype1 : FTtype M != 1%N. Proof. exact: FTtypeP_neq1 MtypeP. Qed.
-Let Mtype34 : FTtype M \in pred2 3 4.
-Proof.
-by have:= FTtype_range M; rewrite -mem_iota !inE !orbA orbC 3?[_ == _](negPf _).
-Qed.
-Let Mtype_gt2 : (FTtype M > 2)%N. Proof. by case/pred2P: Mtype34 => ->. Qed.
-
-Local Notation H0 := (Ptype_Fcore_kernel MtypeP).
-Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope.
-Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
-Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
-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 H := `M`_\F%G.
-Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope.
-Local Notation HU := M^`(1)%G.
-Local Notation "` 'HU'" := `M^`(1)%g (at level 0) : group_scope.
-Local Notation U' := U^`(1)%G.
-Local Notation "` 'U''" := `U^`(1)%g (at level 0) : group_scope.
-Local Notation C := 'C_U(`H)%G.
-Local Notation "` 'C'" := 'C_`U(`H) (at level 0) : group_scope.
-Local Notation HC := (`H <*> `C)%G.
-Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope.
-Local Notation H0C := (`H0 <*> `C)%G.
-Local Notation "` 'H0C'" := (`H0 <*> `C) (at level 0) : group_scope.
-Local Notation Hbar := (`H / `H0)%g.
-
-Local Notation S_ := (seqIndD HU M HU).
-Local Notation tau := (FT_Dade0 maxM).
-Local Notation R := (FTtypeP_coh_base maxM MtypeP).
-Local Notation V := (cyclicTIset defW).
-
-Let Mtype24 := compl_of_typeII_IV maxM MtypeP notMtype5.
-
-Let defMs : M`_\s = HU. Proof. exact: FTcore_type_gt2. Qed.
-Let defA1 : 'A1(M) = HU^#. Proof. by rewrite /= -defMs. Qed.
-Let defA : 'A(M) = HU^#. Proof. by rewrite FTsupp_eq1. Qed.
-Let sHU_A0 : HU^# \subset 'A0(M). Proof. by rewrite -defA FTsupp_sub0. Qed.
-
-Let calS := seqIndD HU M M`_\s 1.
-Let scohM : subcoherent calS tau R. Proof. exact: FTtypeP_subcoherent. Qed.
-Let scoh1 : subcoherent (S_ 1) tau R.
-Proof. by rewrite -{2}(group_inj defMs). Qed.
-
-Let p := #|W2|.
-Let pr_p : prime p. Proof. by have [] := FTtypeP_primes maxM MtypeP. Qed.
-Let ntW2 : W2 :!=: 1%g. Proof. by rewrite -cardG_gt1 prime_gt1. Qed.
-Let cycW2 : cyclic W2. Proof. exact: prime_cyclic. Qed.
-Let def_p : pdiv #|Hbar| = p. Proof. exact: typeIII_IV_core_prime. Qed.
-
-Let q := #|W1|.
-Let pr_q : prime q. Proof. by have [] := FTtypeP_primes maxM MtypeP. Qed.
-Let ntW1 : W1 :!=: 1%g. Proof. by rewrite -cardG_gt1 prime_gt1. Qed.
-Let cycW1 : cyclic W1. Proof. exact: prime_cyclic. Qed.
-
-Let defM : HU ><| W1 = M. Proof. by have [[]] := MtypeP. Qed.
-Let defHU : H ><| U = HU. Proof. by have [_ []] := MtypeP. Qed.
-
-Let nsHUM : HU <| M. Proof. exact: gFnormal. Qed.
-Let sHUM : HU \subset M. Proof. exact: gFsub. Qed.
-Let sHHU : H \subset HU. Proof. by have /mulG_sub[] := sdprodW defHU. Qed.
-Let sUHU : U \subset HU. Proof. by have /mulG_sub[] := sdprodW defHU. Qed.
-Let sUM : U \subset M. Proof. exact: subset_trans sUHU sHUM. Qed.
-
-Let coHUq : coprime #|HU| q.
-Proof. by rewrite (coprime_sdprod_Hall_r defM); have [[]] := MtypeP. Qed.
-Let coUq : coprime #|U| q. Proof. exact: coprimeSg coHUq. Qed.
-	
-Let neq_pq : p != q.
-Proof.
-apply: contraTneq coHUq => <-; rewrite coprime_sym prime_coprime ?cardSg //.
-by rewrite -(typeP_cent_compl MtypeP) subsetIl.
-Qed.
-
-Let solHU : solvable HU. Proof. exact: solvableS sHUM (mmax_sol maxM). Qed.
-Let solH : solvable H. Proof. exact: solvableS sHHU solHU. Qed.
-
-Let ltM''HU :  M^`(2)%g \proper HU.
-Proof. by rewrite (sol_der1_proper solHU) // -defMs FTcore_neq1. Qed.
-
-Let frobMtilde : [Frobenius M / M^`(2) = (HU / M^`(2)) ><| (W1 / M^`(2))].
-Proof.
-have [[_ _ _ _] _ _ [_ _ _ sW2M'' prHUW1 ] _] := MtypeP.
-by rewrite Frobenius_coprime_quotient ?gFnormal //; split=> // _ /prHUW1->.
-Qed.
-
-Let defHC : H \x C = HC.
-Proof.
-by have [defHC _ _ _] := typeP_context MtypeP; rewrite /= (dprodWY defHC).
-Qed.
-
-Let nC_UW1 : U <*> W1 \subset 'N(C).
-Proof.
-have /sdprodP[_ _ nHUW1 _] := Ptype_Fcore_sdprod MtypeP.
-by rewrite normsI ?norms_cent // join_subG normG; have [_ []] := MtypeP.
-Qed.
-
-Let nsCM : C <| M.
-Proof.
-rewrite /normal subIset ?sUM //= -{1}(sdprodW (Ptype_Fcore_sdprod MtypeP)).
-by rewrite mulG_subG cents_norm // centsC subsetIr.
-Qed.
-
-Let nsCU : C <| U. Proof. exact: normalS (subsetIl _ _) sUM nsCM. Qed.
-Let nsHC_M : HC <| M. Proof. by rewrite normalY ?gFnormal. Qed.
-Let sHC_HU : HC \subset HU. Proof. by rewrite join_subG sHHU subIset ?sUHU. Qed.
-Let nsHC_HU : HC <| HU. Proof. exact: normalS nsHC_M. Qed.
-
-Let chiefH0 : chief_factor M H0 H.
-Proof. by have [] := Ptype_Fcore_kernel_exists maxM MtypeP notMtype5. Qed.
-
-Let minHbar : minnormal Hbar (M / H0).
-Proof. exact: chief_factor_minnormal. Qed.
-
-Let abelHbar : p.-abelem Hbar.
-Proof.
-have solHbar : solvable (H / H0) by rewrite quotient_sol.
-have [_ _] := minnormal_solvable minHbar (subxx _) solHbar.
-by rewrite /is_abelem def_Ptype_factor_prime.
-Qed.
-
-Let sH0H : H0 \subset H.
-Proof. by have/andP[/maxgroupp/andP[/proper_sub]]:= chiefH0. Qed.
-
-Let nH0M: M \subset 'N(H0).
-Proof. by have /andP[/maxgroupp/andP[]] := chiefH0. Qed.
-
-Let nsH0H : H0 <| H.
-Proof. by rewrite /normal sH0H gFsub_trans. Qed.
-
-Let nsH0C_M : H0C <| M.
-Proof. by rewrite normalY // /normal ?(subset_trans sH0H) ?gFsub. Qed.
-
-Let defH0C : H0 \x C = H0C.
-Proof.
-have /dprodP[_ _ cHC tiHC] := defHC.
-by rewrite dprodEY ?(centsS sH0H) //; apply/trivgP; rewrite -tiHC setSI.
-Qed.
-
-(* Group-theoretic consequences of the coherence and non-coherence theorems   *)
-(* of Sections 5, 9 and 10 for maximal subgroups of type III and IV.          *)
-
-(* This is Peterfalvi (11.3). *)
-Lemma FTtype34_noncoherence : ~ coherent (S_ H0C) M^# tau.
-Proof.
-move=> cohH0C; suff: coherent (S_ 1) M^# tau by apply: FTtype345_noncoherence.
-have /mulG_sub[_ sW1M] := sdprodW defM.
-have [nsHHU _ _ nHU tiHU] := sdprod_context defHU.
-have sHM: H \subset M := gFsub _ _.
-have [sCM sH0C_M]: C \subset M /\ H0C \subset M by rewrite !normal_sub.
-have nH0_C := subset_trans sCM nH0M.
-have sH0C_HC: H0C \subset HC by apply: genS (setSU _ _).
-have defF: HC :=: 'F(M) by have [/dprodWY] := typeP_context MtypeP.
-have{defF} nilHC: nilpotent (HC / 1) by rewrite defF quotient_nil ?Fitting_nil.
-have /bounded_seqIndD_coherence-bounded_coh1 := scoh1.
-apply: bounded_coh1 nilHC cohH0C _; rewrite ?sub1G ?normal1 //.
-have[_ _ /= oHbar] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5.
-rewrite -(index_sdprod defM) -divgS // -(dprod_card defHC) -(dprod_card defH0C).
-rewrite divnMr ?cardG_gt0 // divg_normal // oHbar def_p -/q.
-by rewrite lbound_expn_odd_prime ?mFT_odd.
-Qed.
-
-(* This is Peterfalvi (11.4). *)
-Lemma bounded_proper_coherent H1 :
-  H1 <| M -> H1 \proper HU -> coherent (S_ H1) M^# tau ->
-    (#|HU : H1| <= 2 * q * #|U : C| + 1)%N.
-Proof.
-move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU.
-suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC.
-  rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM.
-  congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)).
-  rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC.
-  by rewrite Lagrange ?subsetIl // (sdprod_card defHU) (sdprod_card defM).
-apply/negP/(coherent_seqIndD_bound _ _ scoh1 _ _ _ FTtype34_noncoherence) => //.
-suffices /center_idP->: abelian (HC / H0C) by rewrite genS ?setSU.
-suffices /isog_abelian<-: Hbar \isog HC / H0C by apply: abelem_abelian abelHbar.
-by rewrite /= [`H0C]joingC quotient_sdprodr_isog ?(dprodWsdC defHC).
-Qed.
-
-(* This is Peterfalvi (11.5). *)
-Lemma FTtype34_der2 : M^`(2)%g = HC.
-Proof.
-have [defFM [_ not_cHU] _ _] := typeP_context MtypeP.
-have [_ sW1M _ _ tiHU_W1] := sdprod_context defM.
-have{defFM} sM''_HC: M^`(2)%g \subset HC.
-  by rewrite -defHC defFM; have [_ _ []] := MtypeP.
-have scohM'': subcoherent (S_ M^`(2)) tau R.
-  exact/(subset_subcoherent scoh1)/seqInd_conjC_subset1.
-have cohM'': coherent (S_ M^`(2)) M^# tau.
-  apply: uniform_degree_coherence scohM'' _.
-  apply: all_pred1_constant #|M : HU|%:R _ _; rewrite all_map.
-  apply/allP=> _ /seqIndP[s /setDP[kerM'' _] ->] /=; rewrite inE in kerM''.
-  by rewrite cfInd1 ?gFsub // lin_char1 ?mulr1 ?lin_irr_der1.
-have ubHC: (#|HC : M^`(2)| < 2 * q + 1)%N.
-  rewrite -(ltn_pmul2r (indexg_gt0 U C)) mulnDl mul1n.
-  apply: leq_ltn_trans (_ : 2 * q * #|U : C| + 1 < _)%N; last first.
-    by rewrite ltn_add2l indexg_gt1 subsetIidl not_cHU //; have [] := Mtype24.
-  have {1}->: #|U : C| = #|HU : HC| by apply: index_sdprodr (subsetIl _ _).
-  by rewrite mulnC (Lagrange_index sHC_HU) // bounded_proper_coherent ?gFnormal.
-have regHC_W1: semiregular (HC / M^`(2)) (W1 / M^`(2)).
-  by apply: semiregularS (Frobenius_reg_ker frobMtilde); rewrite quotientS.
-suffices /dvdnP[k Dk]: 2 * q %| #|HC : M^`(2)|.-1.
-  apply: contraTeq ubHC; rewrite -leqNgt eqEsubset sM''_HC -indexg_gt1 addn1.
-  by rewrite -[#|_:_|]prednK // {}Dk !ltnS muln_gt0 => /andP[/leq_pmull->].
-rewrite Gauss_dvd; last by rewrite coprime2n mFT_odd.
-rewrite dvdn2 -subn1 odd_sub // addbT negbK subn1.
-rewrite -card_quotient; last by rewrite (subset_trans sHC_HU) // (der_norm 1).
-have Dq: q = #|W1 / M^`(2)|%g.
-  apply/card_isog/quotient_isog; first by rewrite (subset_trans sW1M) ?gFnorm.
-  by apply/trivgP; rewrite -tiHU_W1 setSI // (der_sub 1).
-rewrite quotient_odd ?mFT_odd //= Dq regular_norm_dvd_pred ?quotient_norms //.
-by rewrite (subset_trans sW1M) ?normal_norm.
-Qed.
-Local Notation defM'' := FTtype34_der2.
-
-(* This is Peterfalvi (11.6). *)
-Lemma FTtype34_facts (H' := H^`(1)%g):
-  [/\ p.-group H, U \subset 'C(H0), H0 :=: H' & C :=: U'].
-Proof.
-have nilH: nilpotent H := Fcore_nil M.
-have /sdprod_context[/andP[_ nHM] sUW1M _ _ _] := Ptype_Fcore_sdprod MtypeP.
-have coH_UW1: coprime #|H| #|U <*> W1| := Ptype_Fcore_coprime MtypeP.
-have [[_ mulHU _ tiHU] [nHU isomHU]] := (sdprodP defHU, sdprod_isom defHU).
-have{sUW1M} cH0U: U \subset 'C(H0).
-  have frobUW1 := Ptype_compl_Frobenius maxM MtypeP notMtype5.
-  have nH0_UW1 := subset_trans sUW1M nH0M; have [_ nH0W1] := joing_subP nH0_UW1.
-  have [coH0_UW1 solH0] := (coprimeSg sH0H coH_UW1, solvableS sH0H solH).
-  have [_ -> //] := Frobenius_Wielandt_fixpoint frobUW1 nH0_UW1 coH0_UW1 solH0.
-  have ->: 'C_H0(W1) = H0 :&: 'C_H(W1) by rewrite setIA (setIidPl sH0H).
-  have nH0C: 'C_H(W1) \subset 'N(H0) by rewrite subIset // normal_norm.
-  rewrite cardMg_TI // -LagrangeMl -card_quotient {nH0C}//.
-  rewrite coprime_quotient_cent ?(coprimeSg sHHU) //=.
-  have [_ -> _] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5.
-  by rewrite (typeP_cent_core_compl MtypeP) def_p.
-have{isomHU} defC: C :=: U'.
-  have [injHquo defHUb] := isomP isomHU.
-  apply: (injm_morphim_inj injHquo); rewrite ?subsetIl ?morphim_der ?der_sub //.
-  rewrite defHUb morphim_restrm -quotientE setIA setIid -quotientMidl /=.
-  by rewrite (dprodW defHC) -defM'' -quotient_der // -mulHU mul_subG ?normG.
-have{coH_UW1} defH0: H0 :=: H'.
-  pose Hhat := (H / H')%g; pose Uhat := (U / H')%g; pose HUhat := (HU / H')%g.
-  have nH'H: H \subset 'N(H') by apply: gFnorm.
-  have nH'U: U \subset 'N(H') by apply: gFnorm_trans.
-  apply/eqP; rewrite eqEsubset andbC.
-  rewrite der1_min ?(abelem_abelian abelHbar) ?normal_norm //=.
-  rewrite -quotient_sub1 /= -/H'; last exact: subset_trans sH0H nH'H.
-  suffices <-: 'C_Hhat(Uhat) = 1%g.
-    by rewrite subsetI quotientS //= quotient_cents // centsC.
-  suffices: ~~ ('C_Hhat(Uhat)^`(1)%g \proper 'C_Hhat(Uhat)).
-    exact: contraNeq (sol_der1_proper (quotient_sol _ solH) (subsetIl Hhat _)).
-  have {2}<-: HUhat^`(1)%g :&: 'C_Hhat(Uhat) = 'C_Hhat(Uhat).
-    rewrite -quotient_der ?[HU^`(1)%g]defM''; last by rewrite -mulHU mul_subG.
-    by rewrite (setIidPr _) ?subIset // quotientS ?joing_subl.
-  suffices defHUhat: 'C_Hhat(Uhat) \x ([~: Hhat, Uhat] <*> Uhat) = HUhat.
-    rewrite -(dprod_modl (der_dprod 1 defHUhat)) ?der_sub //= -/Hhat.
-    rewrite [rhs in _ \x rhs](trivgP _) ?dprodg1 ?properxx //= -/Hhat.
-    by have [_ _ _ <-] := dprodP defHUhat; rewrite setIC setIS ?der_sub.
-  have coHUhat: coprime #|Hhat| #|Uhat|.
-    by rewrite coprime_morph ?(coprimegS _ coH_UW1) ?joing_subl.
-  have defHhat: 'C_Hhat(Uhat) \x [~: Hhat, Uhat] = Hhat.
-    by rewrite dprodC coprime_abelian_cent_dprod ?der_abelian ?quotient_norms.
-  rewrite /HUhat -(sdprodWY defHU) quotientY //= -(dprodWY defHhat).
-  have [_ _ cCRhat tiCRhat] := dprodP defHhat.
-  rewrite dprodEY ?joingA //; first by rewrite join_subG cCRhat centsC subsetIr.
-  apply/trivgP; rewrite /= joingC norm_joinEl ?commg_normr //= -/Hhat -/Uhat.
-  rewrite -tiCRhat !(setIAC _ 'C(_)) setSI // subsetI subsetIl /=.
-  by rewrite -group_modr ?commg_subl ?quotient_norms //= coprime_TIg ?mul1g.
-suffices{defC defH0}: p.-group H by [].
-pose R := 'O_p^'(H); have hallR: p^'.-Hall(H) R := nilpotent_pcore_Hall _ nilH.
-have defRHp: R \x 'O_p(H) = H by rewrite dprodC nilpotent_pcoreC.
-suffices R_1: R :=: 1%g by rewrite -defRHp R_1 dprod1g pcore_pgroup.
-have /subsetIP[sRH cUR]: R \subset 'C_H(U).
-  have oH: #|H| = (p ^ q * #|'C_H(U)|)%N.
-    by have:= typeII_IV_core maxM MtypeP notMtype5 => /=; rewrite ifN => // -[].
-  apply/setIidPl/eqP; rewrite eqEcard subsetIl /= (card_Hall hallR) {}oH.
-  rewrite (card_Hall (setI_normal_Hall _ hallR _)) ?subsetIl ?gFnormal //.
-  rewrite partnM ?expn_gt0 ?cardG_gt0 //= part_p'nat ?mul1n ?pnatNK //.
-  by rewrite pnat_exp ?pnat_id.
-suffices: ~~ (R^`(1)%g \proper R) by apply: contraNeq (sol_der1_proper solH _).
-have /setIidPr {2}<-: R \subset HU^`(1)%g.
-  by rewrite [HU^`(1)%g]defM'' -(dprodWY defHC) sub_gen ?subsetU ?sRH.
-suffices defRHpU: R \x ('O_p(H) <*> U) = HU.
-  rewrite -(dprod_modl (der_dprod 1 defRHpU)) ?der_sub //= -/R setIC.
-  rewrite [rhs in _ \x rhs](trivgP _) ?dprodg1 ?properxx //= -/R.
-  by have /dprodP[_ _ _ <-] := defRHpU; rewrite setIS ?der_sub.
-rewrite -(sdprodWY defHU) -[in RHS](dprodWY defRHp) -joingA.
-have [_ _ cRHp tiRHp] := dprodP defRHp.
-rewrite dprodEY //= -/R; first by rewrite join_subG cRHp centsC.
-rewrite joingC norm_joinEl 1?gFnorm_trans //.
-by rewrite -(setIidPl sRH) -setIA -group_modr ?gFsub // tiHU mul1g.
-Qed.
-
-Let frobUW1bar : [Frobenius U <*> W1 / C = (U / C) ><| (W1 / C)].
-Proof.
-have frobUW1: [Frobenius U <*> W1 = U ><| W1].
-  exact: Ptype_compl_Frobenius MtypeP notMtype5.
-have [defUW1 ntU _ _ _] := Frobenius_context frobUW1.
-have [[_ _ _ defC] regUW1] := (FTtype34_facts, Frobenius_reg_ker frobUW1).
-rewrite Frobenius_coprime_quotient // /normal ?subIset ?joing_subl //.
-by split=> [|x /regUW1->]; rewrite ?sub1G //= defC (sol_der1_proper solHU).
-Qed.
-
-(* This is Peterfalvi (11.7).                                                 *)
-(* We have recast the linear algebra arguments in the original text in pure-  *)
-(* group-theoretic terms: the overhead of the abelem_rV correspondence is not *)
-(* justifiable here, as the Ssreflect linear algebra library lacks specific   *)
-(* support for bilinear forms: we use D y z := [~ coset Q y, coset Q z] as    *)
-(* our "linear form". D is antisymmetric as D z y = (D y z)^-1, so we only    *)
-(* show that D is "linear" in z, that is, that D y is a group morphism with   *)
-(* domain H whose kernel contains H0, when y \in H, and we do not bother to   *)
-(* factor D to obtain a form over Hbar = H / H0.                              *)
-(*   We further rework the argument to support this change in perspective:    *)
-(*  - We remove any reference to linear algebra in the "Galois" (9.7b) case,  *)
-(*    where U acts irreducibly on Hbar: we revert to the proof of the         *)
-(*    original Odd Order paper, using the fact that H / Q is extraspecial.    *)
-(*  - In the "non-Galois" (9.7a) case, we use the W1-conjugation class of a   *)
-(*    generator of H1 as an explicit basis of Hbar, indexed by W1, and we     *)
-(*    use the elements xbar_ w = coset H0 (x_ w) of this basis instead of     *)
-(*    arbitrary y in H_i, as the same argument then justifies extending       *)
-(*    commutativity to all of Hbar.                                           *)
-(*  - We construct phi as the morphism mapping ubar in Ubar to the n such     *)
-(*    that the action of ubar on H1 is exponentiation by n. We derive a       *)
-(*    morphism phi_ w ubar for the action of Ubar on H1 ^ w, for w in W1, by  *)
-(*    composign with the action QV of W1 on Ubar by inverse conjugation.      *)
-(*  - We exchange the two alternatives in the (9.7a) case; most of proof is   *)
-(*    thus by contradiction with the C_U(Hbar) != u assertion in (9.6),       *)
-(*    first establishing case 9.7a (as 9.7b contradicts q odd), then that D   *)
-(*    is nontrivial for some x_ w1 and x_ w2 (as (H / Q)' = H0 / Q != 1),     *)
-(*    whence (phi_ w1 u)(phi_ w2 u) = 1, whence (phi u)^-1 = phi u and        *)
-(*    phi = 1, i.e., Ubar centralises Wbar.                                   *)
-(* Note finally that we simply construct U as a maximal subgroup of H0 normal *)
-(* in H, as the nilpotence of H / Q implies that H0 / Q lies in its center.   *)
-Lemma FTtype34_Fcore_kernel_trivial :
-  [/\ p.-abelem H, #|H| = (p ^ q)%N & `H0 = 1%g].
-Proof.
-have [[_ _ nHU tiHU] [pH cH0U defH' _]] := (sdprodP defHU, FTtype34_facts).
-have [/mulG_sub[_ sW1M] nH0H] := (sdprodW defM, normal_norm nsH0H).
-have nHW1: W1 \subset 'N(H) := subset_trans sW1M (gFnorm _ M).
-have nUW1: W1 \subset 'N(U) by have [_ []] := MtypeP.
-pose bar := coset_morphism H0; pose Hbar := (H / H0)%g; pose Ubar := (U / H0)%g.
-have [Cbar_neqU _ /= oHbar] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5.
-rewrite -/Hbar def_p // -/q in oHbar.
-have [nH0U nH0W1] := (subset_trans sUM nH0M, subset_trans sW1M nH0M).
-suffices H0_1 : `H0 = 1%g.
-  have isoHbar: H \isog H / H0 by rewrite H0_1 quotient1_isog.
-  by rewrite (isog_abelem isoHbar) (card_isog isoHbar).
-apply: contraNeq Cbar_neqU => ntH0; rewrite [Ptype_Fcompl_kernel _]unlock.
-suffices: Hbar \subset 'C(Ubar).
-  by rewrite (sameP eqP setIidPl) sub_astabQ nH0U centsC.
-have pH0 := pgroupS sH0H pH; have{ntH0} [_ _ [k oH0]] := pgroup_pdiv pH0 ntH0.
-have{k oH0} [Q maxQ nsQH]: exists2 Q : {group gT}, maximal Q H0 & Q <| H.
-  have [Q [sQH0 nsQH oQ]] := normal_pgroup pH nsH0H (leq_pred _).
-  exists Q => //; apply: p_index_maximal => //.
-  by rewrite -divgS // oQ oH0 pfactorK //= expnS mulnK ?expn_gt0 ?cardG_gt0.
-have nsQH0: Q <| H0 := p_maximal_normal (pgroupS sH0H pH) maxQ.
-have [[sQH0 nQH0] nQH] := (andP nsQH0, normal_norm nsQH).
-have nQU: U \subset 'N(Q) by rewrite cents_norm ?(centsS sQH0).
-pose hat := coset_morphism Q; pose Hhat := (H / Q)%g; pose H0hat := (H0 / Q)%g.
-have{maxQ} oH0hat: #|H0hat| = p by rewrite card_quotient ?(p_maximal_index pH0).
-have defHhat': Hhat^`(1)%g = H0hat by rewrite -quotient_der -?defH'.
-have ntH0hat: H0hat != 1%g by rewrite -cardG_gt1 oH0hat prime_gt1.
-have pHhat: p.-group Hhat by apply: quotient_pgroup.
-have nsH0Hhat: H0hat <| Hhat by apply: quotient_normal.
-have sH0hatZ: H0hat \subset 'Z(Hhat).
-  by rewrite prime_meetG ?oH0hat // meet_center_nil ?(pgroup_nil pHhat).
-have{pHhat} gal'M: ~~ typeP_Galois MtypeP.
-  have sZHhat: 'Z(Hhat) \subset Hhat := center_sub _.
-  have nsH0hatZ: H0hat <| 'Z(Hhat) := normalS sH0hatZ sZHhat nsH0Hhat.
-  have [f injf im_f] := third_isom sQH0 nsQH nsH0H.
-  have fHhat: f @* (Hhat / H0hat) = Hbar by rewrite im_f.
-  apply: contra (odd (logn p #|Hhat|)) _ _; last first.
-    rewrite -(divnK (cardSg (quotientS Q sH0H))) divg_normal // oH0hat.
-    by rewrite -(card_injm injf) // fHhat oHbar -expnSr pfactorK //= mFT_odd.
-  rewrite /typeP_Galois acts_irrQ // => /mingroupP[_ minUHbar].
-  suffices /(card_extraspecial pHhat)[n _ ->]: extraspecial Hhat.
-    by rewrite pfactorK //= odd_double.
-  have abelH: p.-abelem (Hhat / H0hat)%g by rewrite -(injm_abelem injf) ?fHhat.
-  suffices{abelH} defZHhat: 'Z(Hhat) = H0hat.
-    do 2?split; rewrite defZHhat ?oH0hat //.
-    apply/eqP; rewrite eqEsubset (Phi_min pHhat) ?normal_norm //=.
-    by rewrite (Phi_joing pHhat) defHhat' joing_subl.
-  apply: contraNeq ntH0hat; rewrite eqEsubset sH0hatZ andbT => not_esHhat.
-  rewrite -defHhat'; apply/eqP/derG1P/center_idP/(quotient_inj nsH0hatZ)=> //.
-  apply: (injm_morphim_inj injf); rewrite ?quotientS //= fHhat -/Hhat -/H0hat.
-  rewrite minUHbar //= -/Hbar -?fHhat 1?morphim_injm_eq1 ?morphimS // -subG1.
-  rewrite quotient_sub1 ?(normal_norm nsH0hatZ) // not_esHhat -['Z(_)]cosetpreK.
-  rewrite im_f ?sub_cosetpre_quo // quotient_norms ?norm_quotient_pre //.
-  by rewrite gFnorm_trans ?quotient_norms.
-have [H1 []] := typeP_Galois_Pn maxM notMtype5 gal'M.
-rewrite def_p => oH1 nH1Ubar _ /bigdprodWY-defHbar _.
-have /cyclicP[xbar defH1]: cyclic H1 by rewrite prime_cyclic ?oH1.
-have H1xbar: xbar \in H1 by rewrite defH1 cycle_id.
-have sH1_Hbar: H1 \subset Hbar.
-  by rewrite -[Hbar]defHbar (bigD1 1%g) ?group1 ?conjsg1 ?joing_subl.
-have{sH1_Hbar} Hxbar: xbar \in Hbar := subsetP sH1_Hbar xbar H1xbar.
-have /morphimP[x nH0x Hx /= Dxbar] := Hxbar.
-have{oH1} oxbar: #[xbar] = p by rewrite orderE -defH1.
-have memH0: {in H &, forall y z, [~ y, z] \in H0}.
-  by rewrite defH'; apply: mem_commg.
-have [_ /centsP-cHH0hat] := subsetIP sH0hatZ; move/subsetP in nQH.
-pose D y z := [~ hat z, hat y].
-have D_H0_1 y z: y \in H -> z \in H0 -> D y z = 1%g.
-  by move=> Hy H0z; apply/eqP/commgP/cHH0hat; apply: mem_quotient.
-have H0_D: {in H &, forall y z, D y z \in H0hat}.
-  by move=> y z Hy Hz; rewrite -defHhat' mem_commg ?mem_quotient.
-have Dsym y z: (D y z)^-1%g = D z y by rewrite invg_comm.
-have Dmul y: y \in H -> {in H &, {morph D y: z t / z * t}}%g.
-  move=> Hy z t Hz Ht; rewrite {1}/D morphM ?nQH // commMgR; congr (_ * _)%g.
-  by rewrite -{2}morphR ?nQH // -/(D t _) D_H0_1 ?memH0 // mulg1.
-pose Dm y Hy : {morphism H >-> coset_of Q} := Morphism (Dmul y Hy).
-have{D_H0_1} kerDmH0 y Hy: H0 \subset 'ker (Dm y Hy).
-  by rewrite subsetI sH0H; apply/subsetP=> z H0z; rewrite !inE /= D_H0_1.
-pose x_ w := (x ^ w)%g; pose xbar_ w := (xbar ^ bar w)%g.
-move/subsetP in nHW1; move/subsetP in nHU.
-have Hx_ w: w \in W1 -> (x_ w \in H) * {in U, forall u, x_ w ^ u \in H}%g.
-  by move/nHW1=> nHw; split=> [|u /nHU-nHu]; rewrite !memJ_norm.
-have Dx: {in H &, forall y z, {in W1, forall w, D (x_ w) y = 1} -> D y z = 1}%g.
-  move=> y z Hy Hz Dxy1; apply/(kerP (Dm y Hy) Hz); apply: subsetP z Hz.
-  rewrite -(quotientSGK nH0H) ?kerDmH0 // -defHbar gen_subG.
-  apply/bigcupsP=> _ /morphimP[w nH0w W1w ->] /=.
-  rewrite defH1 Dxbar -quotient_cycle -?quotientJ ?quotientS // -cycleJ.
-  by rewrite cycle_subG !inE /= Hx_ //= -Dsym eq_invg1 Dxy1.
-pose ntrivD := [exists w in [predX W1 & W1], #[D (x_ w.1) (x_ w.2)] == p].
-have{ntrivD Dx} /exists_inP[[w1 w2] /andP/=[Ww1 Ww2] /eqP-oDx12]: ntrivD.
-  apply: contraR ntH0hat => Dx_1; rewrite -defHhat' -subG1 gen_subG.
-  apply/subsetP=> _ /imset2P[_ _ /morphimP[y ? Hy ->] /morphimP[z ? Hz ->] ->].
-  apply/set1P/Dx=> // w2 Ww2; rewrite Dx ?Hx_ // => w1 Ww1.
-  have abelH0hat: p.-abelem H0hat by apply: prime_abelem.
-  apply: contraNeq Dx_1 => /(abelem_order_p abelH0hat)oDx12.
-  by apply/exists_inP; exists (w1, w2); rewrite ?inE ?Ww1 // oDx12 ?H0_D ?Hx_.
-have /subsetP-nUW1bar: (W1 / H0)%g \subset 'N(Ubar) := quotient_norms H0 nUW1.
-move/subsetP in nH0H; move/subsetP in nH0W1.
-pose n (phi : {morphism Ubar >-> {unit 'F_p}}) ubar : nat := val (phi ubar).
-have [phi Dphi]: {phi | {in Ubar, forall ub, xbar ^ ub =xbar ^+ n phi ub}}%g.
-  pose xbar_Autm := invm (injm_Zp_unitm xbar).
-  have /restrmP[phi [Dphi _ _ _]]: Ubar \subset 'dom (xbar_Autm \o conj_aut H1).
-    by rewrite -sub_morphim_pre //= im_Zp_unitm -defH1 Aut_conj_aut.
-  rewrite /n pdiv_id // -oxbar; exists phi => ubar /(subsetP nH1Ubar)Uubar.
-  transitivity (Zp_unitm (phi ubar) xbar); last by rewrite autE /= -?defH1.
-  by rewrite Dphi invmK ?im_Zp_unitm -?defH1 ?Aut_aut ?norm_conj_autE.
-pose QV ubar w := (ubar ^ (bar w)^-1)%g.
-have UbarQV: {in Ubar & W1, forall ubar w, QV ubar w \in Ubar}.
-  by move=> ub w Uub W1w; rewrite /= memJ_norm ?groupV ?nUW1bar ?mem_quotient.
-pose phi_ w ub := phi (QV ub w); pose nphi_ w ub := n phi (QV ub w).
-have xbarJ: {in W1 & Ubar, forall w ub, xbar_ w ^ ub = xbar_ w ^+ nphi_ w ub}%g.
-  by move=> w ubar * /=; rewrite -conjgM conjgCV conjgM Dphi ?UbarQV // conjXg.
-have{oDx12} phi_w12 ubar: ubar \in Ubar -> (phi_ w1 ubar * phi_ w2 ubar = 1)%g.
-  pose n_u := nphi_ ^~ ubar => Uubar; have [u nH0u Uu Dubar] := morphimP Uubar.
-  suffices: n_u w1 * n_u w2 == 1 %[mod #[D (x_ w1) (x_ w2)]].
-    by apply: contraTeq; rewrite oDx12 -!val_Fp_nat // natrM !natr_Zp.
-  have DXn: {in H & W1, forall y w, D y (x_ w) ^+ n_u w = D y (x_ w ^ u)}%g.
-    move=> y w Hy W1w; set z := x_ w; have [Hz /(_ u Uu) Hzu] := Hx_ w W1w.
-    rewrite -(morphX (Dm y Hy)) //; apply/rcoset_kerP; rewrite ?groupX //.
-    have /subsetP: H0 :* z ^ u \subset 'ker (Dm y Hy) :* z ^ u by rewrite mulSg.
-    apply; apply/rcoset_kercosetP; rewrite ?groupX ?nH0H //.
-    by rewrite morphX ?morphJ ?(nH0W1 w) // ?nH0H //= -Dubar -Dxbar xbarJ.
-  rewrite -eq_expg_mod_order -{1}Dsym expgM expgVn ?(DXn, Dsym) ?Hx_ //.
-  rewrite /D -!morphR ?nQH ?Hx_ // -conjRg (conjg_fixP _) //.
-  by apply/commgP/esym/(centsP cH0U); rewrite ?memH0 ?Hx_.
-pose wbar := bar (w1 * w2 ^-1)%g; pose W1bar := (W1 / H0)%g.
-have W1wbar: wbar \in W1bar by rewrite mem_quotient ?groupM ?groupV.
-have{phi_w12} phiJ: {in Ubar, forall ubar, phi (ubar ^ wbar) = (phi ubar)^-1}%g.
-  move=> ubar Uubar; apply/esym/eqP; rewrite eq_invg_mul.
-  rewrite [wbar]morphM ?morphV ?nH0W1 ?groupV // -{1}[ubar](conjgK (bar w1)).
-  by rewrite conjgM phi_w12 // memJ_norm ?nUW1bar ?mem_quotient.
-have coW1bar2: coprime #|W1bar| 2 by rewrite coprimen2 quotient_odd ?mFT_odd.
-have coUbar2: coprime #|Ubar| 2 by rewrite coprimen2 quotient_odd ?mFT_odd.
-have{wbar phiJ W1wbar} phiV: {in Ubar, forall ubar, phi ubar = (phi ubar)^-1}%g.
-  move=> ubar Uubar; rewrite /= -phiJ // -(expgK coW1bar2 W1wbar) -expgM mul2n.
-  elim: (expg_invn _ _) => [|k IHk]; first by rewrite conjg1.
-  by do 2!rewrite expgSr conjgM phiJ ?memJ_norm ?nUW1bar ?groupX // ?invgK.
-rewrite -[Hbar]defHbar gen_subG defH1; apply/bigcupsP=> _ /morphimP[w _ Ww ->].
-rewrite -cycleJ cycle_subG -/(xbar_ _); apply/centP=> ubar Uubar; apply/commgP.
-apply/conjg_fixP; rewrite xbarJ // /nphi_ -[QV _ w](expgK coUbar2) ?UbarQV //.
-by rewrite /n !morphX ?groupX 1?expgS 1?{1}phiV ?UbarQV // mulVg expg1n.
-Qed.
-
-Let defU' : C :=: U'. Proof. by have [] := FTtype34_facts. Qed.
-Let H0_1 : H0 :=: 1%g. Proof. by have [] := FTtype34_Fcore_kernel_trivial. Qed.
-
-Lemma Ptype_Fcompl_kernel_cent : Ptype_Fcompl_kernel MtypeP :=: C.
-Proof.
-rewrite [Ptype_Fcompl_kernel MtypeP]unlock /= (group_inj H0_1).
-by rewrite astabQ -morphpreIim -injm_cent ?injmK ?ker_coset ?norms1.
-Qed.
-Local Notation defC := Ptype_Fcompl_kernel_cent.
-
-(* Character theory proper. *)
-
-Let pddM := FT_prDade_hyp maxM MtypeP.
-Let ptiWM : primeTI_hypothesis M HU defW := FT_primeTI_hyp MtypeP.
-Let ctiWG : cyclicTI_hypothesis G defW := pddM.
-Let ctiWM : cyclicTI_hypothesis M defW := prime_cycTIhyp ptiWM.
-
-Local Notation sigma := (cyclicTIiso ctiWG).
-Local Notation w_ i j := (cyclicTIirr defW i j).
-Local Notation eta_ i j := (sigma (w_ i j)).
-Local Notation mu_ := (primeTIred ptiWM).
-Local Notation Idelta := (primeTI_Isign ptiWM).
-Local Notation delta_ j := (primeTIsign ptiWM j).
-Local Notation d := (FTtype345_TIirr_degree MtypeP).
-Local Notation n := (FTtype345_ratio MtypeP).
-Local Notation delta := (FTtype345_TIsign MtypeP).
-
-Implicit Types zeta xi lambda : 'CF(M).
-
-Let u := #|U / C|%g.
-Let mu2_ i j := primeTIirr ptiWM i j.
-Let etaW := map sigma (irr W).
-Let eq_proj_eta (alpha gamma : 'CF(G)) := orthogonal (alpha - gamma) etaW.
-Let eta_col j := \sum_i eta_ i j.
-Let bridge0 zeta := mu_ 0 - zeta.
-
-Let proj_col_eta j0 i j : '[eta_col j0, eta_ i j] = (j == j0)%:R.
-Proof.
-rewrite cfdot_suml (bigD1 i) //= cfdot_cycTIiso eqxx eq_sym.
-by rewrite big1 ?addr0 // => k /negPf-i'k; rewrite cfdot_cycTIiso i'k.
-Qed.
-
-Let nirrW1 : #|Iirr W1| = q. Proof. by rewrite card_Iirr_cyclic. Qed.
-Let NirrW1 : Nirr W1 = q. Proof. by rewrite -nirrW1 card_ord. Qed.
-
-Let nirrW2 : #|Iirr W2| = p. Proof. by rewrite card_Iirr_cyclic. Qed.
-Let NirrW2 : Nirr W2 = p. Proof. by rewrite -nirrW2 card_ord. Qed.
-
-Let calT := seqIndT HU M.
-Let S1 := S_ HC.
-Let S2 := seqIndD HU M HC C.
-
-Let sS10 : cfConjC_subset S1 calS.
-Proof. by apply: seqInd_conjC_subset1; rewrite /= ?defMs. Qed.
-
-Let sS20 : cfConjC_subset S2 calS.
-Proof. by apply: seqInd_conjC_subset1; rewrite /= ?defMs. Qed.
-
-Let scohS1 : subcoherent S1 tau R. Proof. exact: subset_subcoherent sS10. Qed.
-Let scohS2 : subcoherent S2 tau R. Proof. exact: subset_subcoherent sS20. Qed.
-
-Let S1_1 : {in S1, forall zeta, zeta 1%g = q%:R}.
-Proof.
-move=> _ /seqIndP[s /setDP[kerM'' _] ->]; rewrite !inE -defM'' in kerM''.
-by rewrite cfInd1 ?gFsub // -(index_sdprod defM) lin_char1 ?mulr1 ?lin_irr_der1.
-Qed.
-
-Let cohS1 : coherent S1 M^# tau.
-Proof.
-apply: uniform_degree_coherence scohS1 _.
-by apply/(@all_pred1_constant _ q%:R)/allP=> _ /=/mapP[zeta /S1_1<- ->].
-Qed.
-
-Let irrS1 : {subset S1 <= irr M}.
-Proof.
-move=> _ /seqIndP[s /setDP[kerHC kerHU] ->]; rewrite !inE in kerHC kerHU.
-rewrite -(quo_IirrK _ kerHC) // mod_IirrE // cfIndMod // cfMod_irr //.
-have /irr_induced_Frobenius_ker := FrobeniusWker frobMtilde; rewrite defM''.
-by apply; rewrite quo_Iirr_eq0 // -subGcfker.
-Qed.
-
-Let o1S1 : orthonormal S1.
-Proof. exact: sub_orthonormal (seqInd_uniq _ _) (irr_orthonormal _). Qed.
-
-Let cfdotS1 : {in S1 &, forall zeta xi, '[zeta, xi] = (zeta == xi)%:R}.
-Proof. by case/orthonormalP: o1S1. Qed.
-
-Let omu2S1 i j : {in S1, forall zeta, '[mu2_ i j, zeta] = 0}.
-Proof.
-move=> zeta S1zeta; have [s _ Dzeta] := seqIndP S1zeta.
-rewrite Dzeta -cfdot_Res_l cfRes_prTIirr cfdot_irr mulrb ifN_eq //.
-apply: contraNneq (prTIred_not_irr ptiWM j) => Ds.
-by rewrite -cfInd_prTIres Ds -Dzeta irrS1.
-Qed.
-
-Let Tmu j : mu_ j \in calT. Proof. by rewrite -cfInd_prTIres mem_seqIndT. Qed.
-
-Let omuS1 j : {in S1, forall zeta,  '[mu_ j, zeta] = 0}.
-Proof.
-by move=> zeta S1zeta /=; rewrite cfdot_suml big1 // => i _; apply: omu2S1.
-Qed.
-
-Let Zbridge0 : {in S1, forall zeta, bridge0 zeta \in 'Z[irr M, HU^#]}.
-Proof.
-have mu0_1: mu_ 0 1%g = q%:R by rewrite prTIred_1 prTIirr0_1 mulr1.
-move=> zeta S1zeta; rewrite /= zcharD1 !cfunE subr_eq0 mu0_1 S1_1 // eqxx.
-by rewrite rpredB ?(seqInd_vchar _ (Tmu 0)) ?(seqInd_vchar _ S1zeta).
-Qed.
-
-Let A0bridge0 : {in S1, forall zeta, bridge0 zeta \in 'CF(M, 'A0(M))}.
-Proof. by move=> zeta /Zbridge0/zchar_on/cfun_onS->. Qed.
-
-Let sS1S2' : {subset S1 <= [predC S2]}.
-Proof.
-by move=> _ /seqIndP[s /setDP[kHCs _] ->]; rewrite !inE mem_seqInd // inE kHCs.
-Qed.
-
-Let defS2: S2 = seqIndD HU M H H0C.
-Proof. by rewrite /S2 H0_1 -!joinGE join1G joinGC seqIndDY. Qed.
-
-Let cohS2: coherent S2 M^# tau.
-Proof.
-apply: subset_coherent (Ptype_core_coherence maxM MtypeP notMtype5).
-by rewrite defC defS2; apply: seqIndS; rewrite Iirr_kerDS ?genS ?setUS ?der_sub.
-Qed.
-
-Let Smu := [seq mu_ j | j in predC1 0].
-Let Sred := filter [predC irr M] (seqIndD HU M H H0).
-
-Let memSred : Sred =i Smu.
-Proof.
-have [szSred _ memSred _] := typeP_reducible_core_Ind maxM MtypeP notMtype5.
-have uSred: uniq Sred by apply: filter_uniq (seqInd_uniq _ _).
-suffices{uSred}: (size Smu <= size Sred)%N by case/leq_size_perm.
-by rewrite szSred def_p size_map -cardE cardC1 nirrW2.
-Qed.
-
-Let mu_1 j : j != 0 -> mu_ j 1%g = (q * u)%:R.
-Proof.
-move=> nzj; have Smuj: mu_ j \in Sred by rewrite memSred image_f.
-have [_ _ _ /(_ _ Smuj)[]] := typeP_reducible_core_Ind maxM MtypeP notMtype5.
-by rewrite defC.
-Qed.
-
-Let memS2red : [predD S2 & irr M] =i Smu.
-Proof.
-move=> xi; rewrite defS2 -memSred mem_filter; apply: andb_id2l => /= red_xi.
-apply/idP/idP=> [|Sxi]; first by apply: seqIndS; rewrite Iirr_kerDS ?joing_subl.
-have [_ _ _ /(_ xi)] := typeP_reducible_core_Ind maxM MtypeP notMtype5.
-by rewrite defC mem_filter /= red_xi; case.
-Qed.
-
-Let i1 : Iirr W1 := inord 1.
-Let nz_i1 : i1 != 0. Proof. by rewrite Iirr1_neq0. Qed.
-Let j1 : Iirr W2 := inord 1.
-Let nz_j1 : j1 != 0. Proof. by rewrite Iirr1_neq0. Qed.
-
-(* This is Peterfalvi (11.8). *)
-(* We have rearranged the argument somewhat:                                  *)
-(* - Step (11.8.4) was out of sequence as it involves changing the definition *)
-(*   of tau2, which requires showing that (11.8.2-3) are preserved by this    *)
-(*   change; since (11.8.4) does not use (11.8.2-3) we avoid this by proving  *)
-(*   (11.8.4) first.                                                          *)
-(* - The first part of step (11.8.3) is the last fact that needs to be proved *)
-(*   for an arbitrary j != 0; (11.8.1, 5-6) can all use the same fixed j != 0 *)
-(*   (we take j = 1), provided (11.8.3) is proved before (11.8.2), which it   *)
-(*   doe not use.                                                             *)
-(* - Steps (11.8.2) and (11.8.5) are really as combination, to provide an     *)
-(*   expression for tau (alpha i j) for an arbitrary i. We merge their proofs *)
-(*   so we can use a fixed i for the whole combined step and hide some        *)
-(*   intermediate technical facts.                                            *)
-(* - We also reorganise the contents of the superstep, proving most of        *)
-(*   (11.8.5) between the first and last two parts of (11.8.2); this          *)
-(*   simplifies the latter because a is then known to be even, so we can show *)
-(*   directly that a is 0 or 2, and then that X = eta i j - eta i 0.          *)
-Lemma FTtype34_not_ortho_cycTIiso zeta :
-  zeta \in S1 -> ~~ eq_proj_eta (tau (bridge0 zeta)) (eta_col 0).
-Proof.
-move=> S1zeta; set psi := tau _; apply/negP=> proj_psi_eta.
-have irr_zeta: zeta \in irr M := irrS1 S1zeta.
-have Szeta: zeta \in S_ 1 by apply: seqInd_sub S1zeta.
-have Zzeta_S1: {in S1, forall xi, zeta - xi \in 'Z[S1, M^#]}.
-  by move=> * /=; rewrite zcharD1E rpredB ?mem_zchar //= !cfunE !S1_1 ?subrr.
-have n1S1: {in S1, forall xi, '[xi] = 1} by move=> xi /irrS1/irrWnorm.
-have Z_S1: {in S1, forall xi, xi \in 'Z[S1]} by apply: mem_zchar.
-have [p_gt0 q_gt0 u_gt0]: [/\ p > 0, q > 0 & u > 0]%N by rewrite !cardG_gt0.
-have q_gt2: (q > 2)%N by rewrite odd_prime_gt2 ?mFT_odd.
-have mu2_1 i j: j != 0 -> mu2_ i j 1%g = d%:R.
-  by have [/(_ i j)] := FTtype345_constants maxM MtypeP notMtype2.
-(* This is (11.8.1). *)
-have [Dd delta1 Dn]: [/\ d = u, delta = 1 & n = (size S1)%:R].
-  have size_S1 : (size S1 * q = u - 1)%N.
-    rewrite mulnC [q](index_sdprod defM).
-      rewrite (size_irr_subseq_seqInd _ (subseq_refl _)) //.
-    transitivity #|[set mod_Iirr t | t : Iirr (HU / HC) in predC1 0]|.
-      apply/eq_card=> s; rewrite inE mem_seqInd // !inE subGcfker.
-      apply/andP/imsetP=> [[nzs kHCs] | [t nzt ->]].
-        by exists (quo_Iirr HC s); rewrite ?quo_IirrK // inE quo_Iirr_eq0.
-      by rewrite mod_Iirr_eq0 // mod_IirrE // cfker_mod.
-    rewrite card_imset; last exact: can_inj (mod_IirrK _).
-    have isoUC: U / C \isog HU / HC by apply: quotient_sdprodr_isog.
-    rewrite subn1 cardC1 card_Iirr_abelian -?(card_isog isoUC) //.
-    by rewrite -(isog_abelian isoUC) defU' der_abelian.
-  have Dd: d = u.
-    apply/eqP; rewrite -(eqn_pmul2l q_gt0) -eqC_nat -(mu_1 nz_j1).
-    by rewrite natrM prTIred_1 mu2_1.
-  suffices delta1: delta = 1.
-    by rewrite /n Dd delta1 -(@natrB _  _ 1) // -size_S1 natrM mulfK ?neq0CG.
-  have: (delta == 1 %[mod q])%C.
-    rewrite -(eqCmod_transl _ (prTIirr1_mod ptiWM 0 j1)) mu2_1 // -/q Dd.
-    by rewrite /eqCmod -(@natrB _ u 1) // dvdC_nat -size_S1 dvdn_mull.
-  rewrite -[1]subr0 [delta]signrE -/ptiWM eqCmodDl eqCmodN opprK.
-  by rewrite eqCmod0_nat; case: (Idelta j1); first rewrite gtnNdvd.
-have deltaZ gamma: delta *: gamma = gamma by rewrite delta1 scale1r.
-have [tau1 coh_tau1] := cohS1; pose zeta1 := tau1 zeta.
-(* This is (11.8.4). *)
-without loss Dpsi: tau1 coh_tau1 @zeta1 / psi = eta_col 0 - zeta1.
-  move=> IHtau1; have [[Itau1 Ztau1] Dtau1] := coh_tau1.
-  have tau1_dirr: {in S1, forall xi, tau1 xi \in dirr G}.
-    by move=> xi S1xi; rewrite /= dirrE Ztau1 ?Itau1 ?mem_zchar //= n1S1.
-  pose chi : 'CF(G) := eta_col 0 - psi.
-  have Dpsi: psi = eta_col 0 - chi by rewrite opprD opprK addNKr.
-  have chi'zeta1: chi <> zeta1.
-    by move=> Dchi; case: (IHtau1 tau1); rewrite -/zeta1 -?Dchi.
-  have dirr_chi: chi \in dirr G.
-    apply: dirr_norm1.
-      rewrite rpredB ?rpred_sum // => [i _|]; first exact: cycTIiso_vchar.
-      rewrite Dade_vchar // zchar_split A0bridge0 //.
-      by rewrite rpredB ?char_vchar ?prTIred_char ?irrWchar.
-    apply: (addrI q%:R); transitivity '[psi]; last first.
-      rewrite Dade_isometry ?A0bridge0 // (cfnormBd (omuS1 _ _)) //.
-      by rewrite cfnorm_prTIred n1S1.
-    rewrite Dpsi [RHS]cfnormDd; last first.
-      rewrite opprB cfdotC cfdot_sumr big1 ?conjC0 // => i _.
-      by rewrite (orthoPl proj_psi_eta) ?map_f ?mem_irr.
-    rewrite cfnormN -nirrW1 -sumr_const cfdot_sumr.
-    by congr (_ + _); apply: eq_bigr => i _; rewrite proj_col_eta.
-  have Dchi: {in S1, forall xi, xi != zeta -> chi = - tau1 xi}.
-    move=> xi S1xi /negPf-zeta'xi; have irr_xi := irrS1 S1xi.
-    suffices: '[zeta1 - tau1 xi, chi] = 1.
-      by case/cfdot_add_dirr_eq1; rewrite ?rpredN ?tau1_dirr.
-    rewrite /= cfdotBr cfdot_sumr big1 => [|i _]; last first.
-      have oS1eta := coherent_ortho_cycTIiso MtypeP sS10 coh_tau1.
-      by rewrite cfdotBl !oS1eta ?irrS1 ?subrr.
-    rewrite -raddfB Dtau1 ?Zzeta_S1 // Dade_isometry ?A0bridge0 //; last first.
-      exact: cfun_onS sHU_A0 (zcharD1_seqInd_on _ (Zzeta_S1 xi S1xi)).
-    rewrite cfdotBr cfdotC cfdotBr 2?omuS1 // subrr conjC0 !sub0r opprK.
-    by rewrite cfdotBl n1S1 // cfdotS1 // zeta'xi subr0.
-  have S1zetaC: zeta^*%CF \in S1 by rewrite cfAut_seqInd.
-  have Dchi_zetaC: chi = - tau1 zeta^*%CF.
-    by rewrite -Dchi ?(seqInd_conjC_neq _ _ _ S1zeta) ?mFT_odd.
-  suffices S1le2: (size S1 <= size [:: zeta; zeta^*%CF])%N.
-    case: (IHtau1 (dual_iso tau1)); last by rewrite /= -Dchi_zetaC.
-    exact: dual_coherence scohS1 coh_tau1 S1le2.
-  rewrite uniq_leq_size ?seqInd_uniq // => xi S1xi.
-  rewrite !inE -implyNb; apply/implyP=> zeta'xi; apply/eqP.
-  apply: (Zisometry_inj Itau1); rewrite ?mem_zchar ?cfAut_seqInd //.
-  by apply: oppr_inj; rewrite -Dchi.
-have [[Itau1 Ztau1] Dtau1] := coh_tau1.
-have tau1_dirr: {in S1, forall xi, tau1 xi \in dirr G}.
-  by move=> xi S1xi; rewrite /= dirrE Ztau1 ?Itau1 ?mem_zchar //= n1S1.
-have oS1eta i j: {in S1, forall xi, '[tau1 xi, eta_ i j] = 0}.
-  by move=> xi S1xi /=; rewrite (coherent_ortho_cycTIiso _ _ coh_tau1) ?irrS1.
-pose alpha_ := FTtype345_bridge MtypeP zeta.
-have A0alpha i j : j != 0 -> alpha_ i j \in 'CF(M, 'A0(M)).
-  by move/supp_FTtype345_bridge->; rewrite ?S1_1.
-have alpha_S1 i j: {in S1, forall xi, '[alpha_ i j, xi] = n *- (xi == zeta)}.
-  move=> xi S1xi; rewrite /= !cfdotBl !cfdotZl !omu2S1 // mulr0 subrr add0r.
-  by rewrite cfdotS1 // eq_sym mulr_natr.
-pose beta_ i j := tau (alpha_ i j) - (eta_ i j - eta_ i 0) + n *: zeta1.
-pose beta := beta_ 0 j1.
-(* This is the first part of (11.8.3). *)
-have betaE i j: j != 0 -> beta_ i j = beta.
-  move=> nz_j; transitivity (beta_ i j1); congr (_ + _); apply/eqP.
-    rewrite eq_sym -subr_eq0 [rhs in _ + rhs]opprD addrACA -opprD subr_eq0.
-    rewrite -linearB /= !opprB !addrA !subrK -!/(mu2_ i _).
-    by rewrite [Dade pddM _]prDade_sub_TIirr ?mu2_1 //= deltaZ.
-  rewrite -subr_eq0 !opprD addrACA -3!opprD opprK subr_eq0 addrACA addrA.
-  rewrite -(prDade_sub2_TIirr pddM) -!/(mu2_ _ _) !deltaZ -linearB /=.
-  by rewrite opprB addrA subrK !deltaZ opprD opprK addrACA addrA.
-pose j := j1. (* The remainder of the proof only uses j = 1. *)
-(* This is the second part of (11.8.3). *)
-have Rbeta: cfReal beta.
-  rewrite /cfReal eq_sym -subr_eq0 rmorphD !rmorphB /= opprB 2!opprD opprB -/j.
-  rewrite 2![(eta_ 0 _)^*%CF]cfAut_cycTIiso -!cycTIirr_aut !aut_Iirr0 -Dade_aut.
-  set k := aut_Iirr conjC j; rewrite -(betaE 0 k) ?aut_Iirr_eq0 // addrACA.
-  rewrite addrC addr_eq0 addrCA subrK opprD opprK Dn raddfZnat -!raddfB /= -Dn.
-  apply/eqP; rewrite (cfConjC_Dade_coherent coh_tau1) ?mFT_odd // -raddfB.
-  rewrite Dtau1 ?Zzeta_S1 ?cfAut_seqInd //= -linearZ scalerBr; congr (tau _).
-  rewrite opprD !rmorphB !deltaZ /= -!prTIirr_aut !aut_Iirr0 addrACA subrr.
-  by rewrite add0r opprK addrC Dn -raddfZnat.
-(* This is the consequence of Peterfalvi (11.8.2) and (11.8.5). *)
-have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1.
-  set phi := tau (alpha_ i j); pose sum_tau1 := \sum_(xi <- S1) tau1 xi.
-  have A0alpha_j k: alpha_ k j \in 'CF(M, 'A0(M)) by apply: A0alpha.
-  have Zphi: phi \in 'Z[irr G].
-    by rewrite Dade_vchar // zchar_split vchar_FTtype345_bridge /=.
-  have [Y S1_Y [X [Dphi oYX oXS1]]] := orthogonal_split (map tau1 S1) phi.
-  (* This is the first part of 11.8.2 *)
-  have [a Za defY]: exists2 a, a \in Cint & Y = a *: sum_tau1 - n *: zeta1.
-    have [a_ Da defY] := orthonormal_span (map_orthonormal Itau1 o1S1) S1_Y.
-    have{Da} Da: {in S1, forall xi, a_ (tau1 xi) = '[phi, tau1 xi]}.
-      by move=> xi Sxi; rewrite Da Dphi cfdotDl (orthoPl oXS1) ?map_f ?addr0.
-    exists (a_ (tau1 zeta) + n).
-      by rewrite Dn rpredD ?rpred_nat // Da // Cint_cfdot_vchar ?Ztau1 ?Z_S1.
-    rewrite defY big_map scaler_sumr !(bigD1_seq _ S1zeta) ?seqInd_uniq //=.
-    rewrite addrAC scalerDl addrK !(big_seq_cond (predC1 _)) /=; congr (_ + _).
-    apply: eq_bigr => xi /andP[S1xi zeta'xi]; congr (_ *: _); rewrite !Da //.
-    apply: canRL (addNKr _) _; rewrite addrC -opprB -!raddfB Dtau1 ?Zzeta_S1//=.
-    rewrite Dade_isometry //; last first.
-      exact: cfun_onS (zcharD1_seqInd_on _ (Zzeta_S1 _ S1xi)).
-    by rewrite cfdotBr !alpha_S1 // !mulrb eqxx ifN_eq // !(addr0, opprK).
-  have psi_phi: '[psi, phi] = -1 + n. (* This is part of (11.8.5). *)
-    rewrite cfdotC Dade_isometry ?A0bridge0 //.
-    rewrite cfdotBr !cfdotBl deltaZ !cfdotZl n1S1 // mulr1.
-    rewrite !cfdot_prTIirr_red (negPf nz_j1) eqxx !omu2S1 //= cfdotC omuS1 //.
-    by rewrite conjC0 mulr0 opprB !subr0 add0r rmorphD rmorphN Dn !rmorph_nat.
-  have{psi_phi} col0_beta: '[eta_col 0, beta] = a. (* Also part of (11.8.5). *)
-    apply/(addIr (-1 + n))/(canRL (addNKr _)).
-    rewrite addrCA addrA addrACA -{}psi_phi Dpsi cfdotBl; congr (_ + _).
-      rewrite -(betaE i j) // cfdotDr !cfdotBr -/phi cfdotZr -!addrA.
-      apply/(canLR (addNKr _)); rewrite addNr !cfdot_suml.
-      rewrite big1 ?add0r ?opprK => [|k _]; last first.
-        by rewrite cfdot_cycTIiso andbC eq_sym (negPf nz_j1).
-      rewrite addrCA big1 ?mulr0 ?add0r => [|k _]; last first.
-        by rewrite cfdotC oS1eta ?conjC0.
-      rewrite addrC (bigD1 i) // cfnorm_cycTIiso /= addKr big1 // => k i'k.
-      by rewrite cfdot_cycTIiso (negPf i'k).
-    rewrite cfdotC Dphi cfdotDl (orthoPl oXS1) ?map_f // addr0.
-    rewrite defY cfdotBl scaler_sumr cfproj_sum_orthonormal //.
-    rewrite cfdotZl Itau1 ?mem_zchar ?n1S1 // mulr1 rmorphB opprD opprK.
-    by rewrite Dn rmorph_nat conj_Cint.
-    have a_even: (2 %| a)%C. (* Third internal part of (11.8.5). *)
-    have Zbeta: beta \in 'Z[irr G].
-      rewrite -{1}(betaE i j) // rpredD ?rpredB ?Zphi ?cycTIiso_vchar //.
-      by rewrite Dn rpredZnat // Ztau1 ?mem_zchar.
-    rewrite -col0_beta cfdot_real_vchar_even ?mFT_odd //; first 1 last.
-      split; first by apply/rpred_sum=> k _; apply: cycTIiso_vchar.
-      apply/eqP; rewrite [RHS](reindex_inj (can_inj (@conjC_IirrK _ _))) /=.
-      rewrite rmorph_sum; apply/eq_bigr=> k _ /=.
-      by rewrite cfAut_cycTIiso -cycTIirr_aut aut_Iirr0.
-    have eta00: eta_ 0 0 = 1 by rewrite cycTIirr00 cycTIiso1.
-    rewrite orbC cfdotDl 2!cfdotBl cfdotZl -eta00 oS1eta // mulr0 addr0.
-    rewrite opprB addrC 2!{1}cfdot_cycTIiso (negPf nz_j1) subr0 /= eta00.
-    rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE.
-    rewrite cfRes_cfun1 !cfdotBl deltaZ !cfdotZl -!/(mu2_ 0 _).
-    rewrite -(prTIirr00 ptiWM) !cfdot_prTIirr cfdotC omu2S1 // conjC0 mulr0.
-    by rewrite (negPf nz_j1) add0r subr0 subrr rpred0.
-  have nY: '[Y] = n * a * (a - 2%:R) + n ^+ 2. (* Resuming step (11.8.2). *)
-    rewrite defY cfnormD cfnormN !cfnormZ cfdotNr cfdotZr.
-    rewrite cfnorm_map_orthonormal // -Dn Itau1 ?mem_zchar ?n1S1 // mulr1.
-    rewrite scaler_sumr cfproj_sum_orthonormal // rmorphN addrAC.
-    rewrite Dn rmorphM !Cint_normK ?rpred_nat // !rmorph_nat conj_Cint // -Dn.
-    by rewrite -mulr2n mulrC mulrA -mulr_natr mulNr -mulrBr.
-  have{a_even} Da: (a == 0) || (a == 2%:R). (* Second part of (11.8.2). *)
-    suffices (b := a - 1): b ^+ 2 == 1.
-      by rewrite -!(can_eq (subrK 1) a) add0r addrK orbC -eqf_sqr expr1n.
-    have S1gt0: (0 < size S1)%N by case: (S1) S1zeta.
-    have: n * b ^+ 2 <= n *+ 3.
-      have: 2%:R + n <= n *+ 3 by rewrite addrC ler_add2l ler_muln2r Dn ler1n.
-      apply: ler_trans; rewrite sqrrB1 -mulr_natr -mulrBr mulrDr mulrA mulr1.
-      rewrite ler_add2r -(ler_add2r (n ^+ 2 + '[X])) !addrA -nY -cfnormDd //.
-      by rewrite -Dphi norm_FTtype345_bridge ?S1_1 // ler_addl cfnorm_ge0.
-    have Zb: b \in Cint by rewrite rpredB ?rpred1 ?Za.
-    have nz_b: b != 0 by rewrite subr_eq0 (memPn _ a a_even) ?(dvdC_nat 2 1).
-    rewrite eqr_le sqr_Cint_ge1 {nz_b}//= andbT -Cint_normK // Dn -mulrnA.
-    have /CnatP[m ->] := Cnat_norm_Cint Zb; rewrite -natrX -natrM leC_nat.
-    by rewrite leq_pmul2l // lern1 -ltnS (ltn_sqr m 2) (leq_sqr m 1).
-  have{nY Da} defX: X = eta_ i j - eta_ i 0. (* Last part of (11.8.2). *)
-    have{nY Da} /eqP-nY: '[Y] == n ^+ 2.
-      by rewrite -subr_eq0 nY addrK -mulrA !mulf_eq0 !subr_eq0 Da orbT.
-    have coh_zeta_phi := FTtype345_bridge_coherence _ _ Szeta _ coh_tau1.
-    have:= Dphi; rewrite addrC => /coh_zeta_phi->; rewrite ?S1_1 ?deltaZ //.
-    rewrite defY scaler_sumr big_seq rpredB ?rpred_sum // => [xi Sxi|].
-      by rewrite rpredZ_Cint ?mem_zchar ?map_f.
-    by rewrite Dn rpredZnat ?mem_zchar ?map_f.
-  have{col0_beta} a0: a = 0. (* This is the conclusion of (11.8.5). *)
-    rewrite cfdot_suml big1 // in col0_beta => k _.
-    rewrite -(betaE i j) // /beta_ -/phi Dphi -defX addrK defY subrK.
-    rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 // => xi S1xi.
-    by rewrite cfdotC oS1eta ?conjC0.
-  by rewrite Dphi defY defX a0 ?inE ?eqxx // scale0r sub0r addrC.
-(* This is step (11.8.6). *)
-pose theta := mu_ j - d%:R *: zeta.
-have /andP/=[red_muj S2muj]: mu_ j \in [predD S2 & irr M].
-  by rewrite memS2red image_f.
-have HUtheta: theta \in 'CF(M, HU^#).
-  rewrite cfun_onD1 !cfunE mu_1 ?S1_1 // Dd mulrC natrM subrr eqxx.
-  by rewrite rpredB ?rpredZ ?(seqInd_on _ S1zeta) ?(seqInd_on _ S2muj).
-have Dtheta: theta = mu_ 0 - zeta + \sum_i alpha_ i j.
-  rewrite !sumrB -scaler_sumr delta1 scale1r.
-  rewrite [X in _ = X]addrC -!addrA -/(mu_ 0); congr (_ + _).
-  rewrite [X in _ = _ + X]addrC !addrA addNr add0r -opprD; congr (- _).
-  rewrite sumr_const nirrW1 -scaler_nat scalerA mulrC.
-  by rewrite divfK ?neq0CG // delta1 addrC scalerBl scale1r subrK.
-have tau_theta: tau theta = eta_col j - d%:R *: zeta1.
-  pose psi1 i := eta_ i j1 - eta_ i 0 - n *: zeta1.
-  have Dpsi1 i: tau (alpha_ i j) = psi1 i by apply: tau_alpha.
-  rewrite Dtheta [tau _]raddfD raddf_sum (eq_bigr psi1) //= {Dpsi1}/psi1 -/psi.
-  rewrite Dpsi !sumrB  [X in X = _]addrC -!addrA; congr (_ + _).
-  rewrite -opprB -opprD -opprB -/(eta_col 0) addrA addrK; congr (- _).
-  rewrite sumr_const nirrW1 -scaler_nat scalerA mulrC.
-  by rewrite divfK ?neq0CG // delta1 scalerBl scale1r subrK.
-have [tau2 coh_tau2] := cohS2.
-without loss tau2muj: tau2 coh_tau2 / tau2 (mu_ j) = eta_col j; last first.
-  case: FTtype34_noncoherence; rewrite H0_1 -joinGE join1G.
-  have uS12: uniq (S2 ++ S1).
-    by rewrite cat_uniq ?seqInd_uniq ?andbT //=; apply/hasPn.
-  have /perm_eq_coherent: perm_eq (S2 ++ S1) (S_ C); last apply.
-    apply: uniq_perm_eq; rewrite ?seqInd_uniq // => xi; rewrite mem_cat.
-    apply/idP/idP=> [/orP | /seqIndP[i /setDP[kCi k'HUi] ->]].
-      by case; apply/seqIndS/Iirr_kerDS; rewrite ?joing_subr.
-    by rewrite !mem_seqInd // inE orbC inE kCi k'HUi andbT orbN.
-  move: tau_theta; rewrite -tau2muj // -raddfZnat.
-  apply: (bridge_coherent scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2' _.
-  by rewrite (cfun_onS _ HUtheta) ?setSD // rpredZnat ?Z_S1.
-move=> IHtau2; apply: (IHtau2 tau2 coh_tau2); have [IZtau2 Dtau2] := coh_tau2.
-have{IHtau2} /hasP[xi S2xi /=irr_xi]: has [mem irr M] S2.
-  apply/hasPn=> redS2 {tau2 coh_tau2 IZtau2 Dtau2}.
-  have muS2: {subset S2 <= Smu} by move=> xi S2xi; rewrite -memS2red !inE redS2.
-  have [_ [tau2 tau2mu coh_tau2]] := uniform_prTIred_coherent pddM nz_j1.
-  have S2uniform: {subset S2 <= uniform_prTIred_seq pddM j}.
-    move=> _ /muS2/imageP[k nz_k ->]; apply: image_f.
-    by rewrite !inE [_ != 0]nz_k /= !mu_1.
-  apply: (IHtau2 tau2); first exact: subset_coherent_with coh_tau2.
-  have [_ /(_ _ nz_j1) Ez _ _] := FTtype345_constants maxM MtypeP notMtype2.
-  by have:= tau2mu j; rewrite Ez -/delta delta1 scale1r.
-suffices: '[tau2 (mu_ j), eta_col j] != 0.
-  have:= FTtypeP_coherent_TIred sS20 coh_tau2 irr_xi S2xi S2muj.
-  case=> _ -> [[-> ->] | [-> -> _] /eqP[]]; first by rewrite deltaZ.
-  rewrite -[cyclicTIiso _]/sigma cfdot_sumr big1 ?mulr0 // => i _.
-  rewrite cfdotZl proj_col_eta -(inj_eq irr_inj) conjC_IirrE eq_sym.
-  by rewrite odd_eq_conj_irr1 ?mFT_odd // irr_eq1 (negPf nz_j1) mulr0.
-pose gamma := xi 1%g *: mu_ j - mu_ j 1%g *: xi.
-have: '[tau2 gamma, tau theta] != 0.
-  have [Txi Tzeta] := (seqInd_subT S2xi, seqInd_subT S1zeta).
-  have S2gamma: gamma \in 'Z[S2, HU^#] by apply: sub_seqInd_zchar.
-  rewrite Dtau2 ?zcharD1_seqInd //; move/zchar_on in S2gamma.
-  rewrite Dade_isometry ?(cfun_onS sHU_A0) // cfdotBr cfdotZr !cfdotBl !cfdotZl.
-  rewrite cfnorm_prTIred omuS1 // (seqInd_ortho _ _ S2muj) ?(memPn red_muj) //.
-  rewrite (seqInd_ortho _ Txi) ?(memPn (sS1S2' _)) // !(mulr0, subr0) mulf_eq0.
-  by rewrite char1_eq0 ?irrWchar // -cfnorm_eq0 irrWnorm ?oner_eq0 ?neq0CG.
-apply: contraNneq => o_muj_etaj; rewrite {}tau_theta !{gamma}raddfB subr_eq0 /=.
-have /CnatP[xi1 ->]: xi 1%g \in Cnat by rewrite Cnat_char1 ?irrWchar.
-rewrite mu_1 // cfdotZr !cfdotBl !raddfZnat !cfdotZl {}o_muj_etaj cfdot_sumr.
-have /orthogonalP oS2_S1: orthogonal (map tau2 S2) (map tau1 S1).
-  exact: (coherent_ortho scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2'.
-rewrite !oS2_S1 ?map_f // big1 ?(mulr0, subr0) // => k _.
-exact: (coherent_ortho_cycTIiso _ _ coh_tau2).
-Qed.
-
-(* This is Peterfalvi (11.9). *)
-(* Note that in the proof of part (a), the text improperly suggests using     *)
-(* (5.3.b) to show then tau (zeta - zeta^alpha) is orthogonal to the eta i j. *)
-(* Since alpha might not be conjugation, this is not obvious. Indeed the best *)
-(* way to derive this is to use (5.5) together with the coherence of S(HC).   *)
-(* In part (c) we start by reducing the proof to q <= p - 1; we also don't    *)
-(* compute [tau (mu0 - zeta), tau2 lambda] = [chi, tau2 lambda] since this    *)
-(* is not needed to prove than u = a: one only needs to show that the         *)
-(* the left-hand side is an integer, which is in fact required to show that   *)
-(* the right-hand is an integer.                                              *)
-Lemma FTtype34_structure (eta0row := \sum_j eta_ 0 j) :
-  [/\ (*a*) {in S1, forall zeta, eq_proj_eta (tau (bridge0 zeta)) eta0row},
-      (*b*) (p < q)%N
-    & (*c*) FTtype M == 3 /\ typeP_Galois MtypeP].
-Proof.
-have sum_etaW F: \sum_(eta <- etaW) F eta = \sum_i \sum_j F (eta_ i j).
-  rewrite big_map big_tuple (reindex (dprod_Iirr defW)) /=.
-    by rewrite pair_bigA; apply: eq_bigr => -[i j].
-  by exists (inv_dprod_Iirr defW) => ij; rewrite ?dprod_IirrK ?inv_dprod_IirrK.
-have bridgeS1: {in S1, forall zeta, eq_proj_eta (tau (bridge0 zeta)) eta0row}.
-  move=> zeta S1zeta; set phi := bridge0 zeta; have irr_zeta := irrS1 S1zeta.
-  have [X etaX [chi [Dchi oXchi o_chi_eta]]] := orthogonal_split etaW (tau phi).
-  have [Isigma Zsigma] := cycTI_Zisometry ctiWG.
-  have{o_chi_eta} o_chi_eta i j: '[chi, eta_ i j] = 0.
-    by rewrite (orthoPl o_chi_eta) ?map_f ?mem_irr.
-  have o1etaW: orthonormal etaW by rewrite map_orthonormal ?irr_orthonormal.
-  have [a Da defX] := orthonormal_span o1etaW etaX; pose a_ := a (eta_ _ _).
-  have{Da} Da i j: a_ i j = '[tau phi, eta_ i j].
-    by rewrite Dchi cfdotDl o_chi_eta addr0 /a_ Da.
-  have Zphi: phi \in 'Z[irr M, HU^#] by apply: Zbridge0.
-  have A0phi: phi \in 'CF(M, 'A0(M)) by apply: A0bridge0.
-  have a00_1 : a_ 0 0 = 1.
-    rewrite Da cycTIirr00 [sigma 1]cycTIiso1.
-    rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE.
-    rewrite rmorph1 /= -(prTIirr00 ptiWM) -/(mu2_ 0 0) cfdotC.
-    by rewrite cfdotBr cfdot_prTIirr_red omu2S1 // subr0 rmorph1.
-  have aut_phi nu: cfAut nu (tau phi) = tau phi + tau (zeta - cfAut nu zeta).
-    rewrite -Dade_aut !rmorphB !raddfB /= !addrA subrK.
-    by rewrite -prTIred_aut aut_Iirr0.
-  have Za i j: a_ i j \in Cint.
-    rewrite Da Cint_cfdot_vchar ?cycTIiso_vchar //.
-    by rewrite Dade_vchar ?(zchar_onS sHU_A0).
-  have [tau1 coh_tau1] := cohS1; have [_ Dtau1] := coh_tau1.
-  have o_tau1_eta := coherent_ortho_cycTIiso MtypeP sS10 coh_tau1.
-  have a_aut nu i j: a (cfAut nu (eta_ i j)) = a_ i j.
-    symmetry; transitivity '[cfAut nu (tau phi), cfAut nu (eta_ i j)].
-      by rewrite cfdot_aut_vchar ?cycTIiso_vchar // -Da aut_Cint.
-    rewrite aut_phi cfAut_cycTIiso -cycTIirr_aut [a _]Da cfdotDl addrC.
-    rewrite -Dtau1 ?zcharD1_seqInd ?seqInd_sub_aut_zchar // raddfB cfdotBl.
-    by rewrite !o_tau1_eta ?cfAut_seqInd ?cfAut_irr // subr0 add0r.
-  pose a10 := a_ i1 0; pose a01 := a_ 0 j1; pose a11 := a_ i1 j1.
-  have Da10 i: i != 0 -> a_ i 0 = a10.
-    case/(cfExp_prime_transitive pr_q nz_i1) => k co_k_wi1 Dwi.
-    rewrite -(cforder_dprodl defW) -dprod_IirrEl in co_k_wi1.
-    have [[nu eta10nu] _] := cycTIiso_aut_exists ctiWG co_k_wi1.
-    by rewrite /a_ dprod_IirrEl Dwi rmorphX /= -dprod_IirrEl eta10nu a_aut.
-  have Da01 j: j != 0 -> a_ 0 j = a01.
-    case/(cfExp_prime_transitive pr_p nz_j1) => k co_k_wj1 Dwj.
-    rewrite -(cforder_dprodr defW) -dprod_IirrEr in co_k_wj1.
-    have [[nu eta01nu] _] := cycTIiso_aut_exists ctiWG co_k_wj1.
-    by rewrite /a_ dprod_IirrEr Dwj rmorphX /= -dprod_IirrEr eta01nu a_aut.
-  have DaB1 i j: a_ i j = a_ i 0 + a_ 0 j - a_ 0 0.
-    apply: (canRL (addrK _)); rewrite !Da cycTIiso_cfdot_exchange // => x Vx.
-    have /setDP[A0x A'x]: x \in 'A0(M) :\: 'A(M).
-      by rewrite (FTsupp0_typeP maxM MtypeP) // mem_class_support.
-    by rewrite Dade_id // (cfun_on0 (zchar_on Zphi)) // -defA.
-  pose p1 : algC := p.-1%:R; pose q1 : algC := q.-1%:R.
-  have normX: '[X] = 1 + q1 * a10 ^+ 2 + p1 * a01 ^+ 2 + p1 * q1 * a11 ^+ 2.
-    transitivity (\sum_i \sum_j a_ i j ^+ 2).
-      rewrite defX cfnorm_sum_orthonormal // sum_etaW.
-      by apply/eq_bigr=> i _; apply/eq_bigr=> j _; rewrite Cint_normK ?Za.
-    rewrite -addrA addrACA (bigD1 0) //= (bigD1 0) //= a00_1 expr1n.
-    rewrite -natrM !mulr_natl mulrnA -mulrnDl.
-    rewrite -nirrW1 -nirrW2 -!(cardC1 0) -!sumr_const.
-    congr (1 + _ + _); first by apply: eq_bigr => j /Da01->.
-    apply: eq_bigr => i /Da10-Dai0; rewrite (bigD1 0) //= Dai0; congr (_ + _).
-    by apply: eq_bigr => j /Da01-Da0j; rewrite DaB1 Dai0 Da0j -DaB1.
-  have normX_le_q: '[X] <= q%:R.
-    rewrite -(ler_add2r '[chi]) -cfnormDd // -Dchi -ler_subl_addl.
-    have ->: '[tau phi] - q%:R = 1.
-      rewrite Dade_isometry ?A0bridge0 // cfnormBd; last by rewrite omuS1.
-      by rewrite cfnorm_prTIred cfdotS1 // eqxx addrC addKr.
-    suffices: '[chi] != 0.
-      suffices /CnatP[nchi ->]: '[chi] \in Cnat by rewrite ler1n lt0n -eqC_nat.
-      rewrite Cnat_cfnorm_vchar // -(canLR (addKr _) Dchi) defX addrC rpredB //.
-         by rewrite Dade_vchar // (zchar_onS (FTsupp_sub0 M)) ?defA.
-       rewrite big_map big_seq rpred_sum // => _ /(cycTIirrP defW)[i [j ->]].
-       by rewrite rpredZ_Cint ?Za ?cycTIiso_vchar.
-    pose theta := zeta - zeta^*%CF.
-    have Ztheta: theta \in 'Z[S1, HU^#] by apply: seqInd_sub_aut_zchar.
-    have: '[tau phi, tau theta] != 0.
-      rewrite Dade_isometry //; last by rewrite (cfun_onS _ (zchar_on Ztheta)).
-      rewrite cfdotBl !cfdotBr ?omuS1 ?cfAut_seqInd // subr0 add0r oppr_eq0.
-      rewrite irrWnorm // (seqInd_conjC_ortho _ _ _ S1zeta) ?mFT_odd //.
-      by rewrite subr0 oner_eq0.
-    rewrite cfnorm_eq0 Dchi; apply: contraNneq => ->; rewrite addr0 defX.
-    rewrite -Dtau1 ?zcharD1_seqInd //.
-    rewrite cfdot_suml big_map big1_seq // => _ /(cycTIirrP defW)[i [j ->]].
-    apply/eqP; rewrite cfdotC fmorph_eq0 cfdotZr raddfB cfdotBl.
-    by rewrite !o_tau1_eta ?cfAut_seqInd ?cfAut_irr // subrr mulr0.
-  have a2_ge0 i j: 0 <= a_ i j ^+ 2 by rewrite -realEsqr Creal_Cint.
-  have a11_0: a11 = 0.
-    have: ('[X] < (2 * q.-1)%:R).
-      rewrite (ler_lt_trans normX_le_q) // ltC_nat -subn1 mulnBr ltn_subRL.
-      by rewrite !mul2n -!addnn ltn_add2r odd_prime_gt2 ?mFT_odd.
-    apply: contraTeq => nz_a11; rewrite ler_gtF // normX ler_paddl //.
-      by rewrite !mulr_natl ?addr_ge0 ?ler01 ?mulrn_wge0 ?a2_ge0.
-    rewrite -mulr_natl -natrM ?ler_pmul ?natr_ge0 ?sqr_Cint_ge1 ?Za //.
-    by rewrite leC_nat leq_mul // -subn1 ltn_subRL odd_prime_gt2 ?mFT_odd.
-  rewrite a11_0 expr0n /= mulr0 addr0 in normX.
-  have a10_a01: a10 + a01 = 1.
-    by apply/eqP; rewrite -subr_eq0 -a00_1 -DaB1 -/a11 a11_0.
-  have{o_chi_eta} o_chi_eta: orthogonal chi etaW.
-    by apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->].
-  have a10_0: a10 = 0.
-    apply: contraNeq (FTtype34_not_ortho_cycTIiso S1zeta) => nz_a10.
-    have a01_0: a01 = 0.
-      apply: contraTeq normX_le_q => nz_a01; rewrite normX ltr_geF //.
-      rewrite ltr_spaddr 1?mulr_gt0 ?ltr0n -?subn1 ?subn_gt0 ?prime_gt1 //.
-        by rewrite ltr_def sqrf_eq0 nz_a01 a2_ge0.
-      rewrite -ler_subl_addl -(natrB _ (prime_gt0 pr_q)) subn1 -mulr_natl.
-      by rewrite ler_wpmul2l ?ler0n // sqr_Cint_ge1 ?Za.
-    suffices <-: X = eta_col 0 by rewrite Dchi /eq_proj_eta addrC addKr.
-    rewrite defX sum_etaW exchange_big (bigD1 0) //= addrC.
-    rewrite big1 ?add0r => [|j nz_j]; first apply: eq_bigr => i _; last first.
-      rewrite (bigD1 0) // [a _]Da01 //= a01_0 scale0r add0r big1 // => i nz_i.
-      by rewrite [a _]DaB1 Da10 // Da01 // a10_a01 a00_1 subrr scale0r.
-    have [-> | nz_i] := eqVneq i 0; first by rewrite [a _]a00_1 scale1r.
-    by rewrite [a _]Da10 // (canRL (addrK _) a10_a01) a01_0 subr0 scale1r.
-  suffices <-: X = eta0row by rewrite Dchi /eq_proj_eta addrC addKr.
-  rewrite defX sum_etaW (bigD1 0) //= addrC.
-  rewrite big1 ?add0r => [|i nz_i]; first apply: eq_bigr => j _; last first.
-    rewrite (bigD1 0) // [a _]Da10 //= a10_0 scale0r add0r big1 // => j nz_j.
-    by rewrite [a _]DaB1 Da10 // Da01 // a10_a01 a00_1 subrr scale0r.
-  have [-> | nz_j] := eqVneq j 0; first by rewrite [a _]a00_1 scale1r.
-  by rewrite [a _]Da01 // (canRL (addKr _) a10_a01) a10_0 oppr0 add0r scale1r.
-have [zeta [irr_zeta Szeta zeta1]] := FTtypeP_ref_irr maxM MtypeP.
-have{zeta1} [S1zeta zeta1]: zeta \in S1 /\ zeta 1%g = q%:R.
-  split=> //; have [k nz_k Dzeta] := seqIndC1P Szeta.
-  rewrite Dzeta mem_seqInd // !inE subGcfker nz_k -defM'' lin_char_der1 //.
-  rewrite -mulr_natl Dzeta cfInd1 //= -(index_sdprod defM) in zeta1.
-  by apply/andP; rewrite irr_char -(mulfI _ zeta1) ?neq0CG.
-have{Szeta} ltpq: (p < q)%N.
-  rewrite ltn_neqAle neq_pq leqNgt /=.
-  apply: contra (FTtype34_not_ortho_cycTIiso S1zeta) => ltqp.
-  case/(FTtype345_Dade_bridge0 _ MtypeP): Szeta => // chi [-> _ _ o_chi_eta].
-  rewrite /eq_proj_eta addrC addKr (orthogonal_oppl chi).
-  by apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->].
-suffices galM: typeP_Galois MtypeP.
-  have [_ [_ _ _ [/= cycUbar _ _]]] := typeP_Galois_P maxM notMtype5 galM.
-  have{cycUbar} cycUbar: cyclic (U / U') by rewrite -defU' -defC.
-  have nilU: nilpotent U by have [_ []] := MtypeP.
-  case/orP: Mtype34 => // /(compl_of_typeIV maxM MtypeP)[_ /negP[]].
-  exact/cyclic_abelian/cyclic_nilpotent_quo_der1_cyclic.
-apply: contraLR ltpq => gal'M; rewrite -leqNgt (leq_trans _ (leq_pred _)) //.
-have [_ _ _] := typeP_nonGalois_characters maxM notMtype5 gal'M.
-case: (_ gal'M) => H1 /= [_ _ nH1U _ []]; set a := #|U : _| => a_gt1.
-rewrite def_p -/q -defU' -defS2 => a_dv_p1 cycUhat _.
-set irr_qa := [pred lambda in irr M | lambda 1%g == (q * a)%:R] => S2_qa.
-have{S2_qa}/hasP[lambda S2lambda /andP[irr_lambda /eqP-lambda1]]: has irr_qa S2.
-  have [a2_dv_pu] := S2_qa; rewrite has_count; apply: leq_trans.
-  rewrite -(@ltn_pmul2r (a ^ 2 * #|C|)); last first.
-    by rewrite !muln_gt0 (ltnW a_gt1) cardG_gt0.
-  by rewrite mul0n divnK // muln_gt0 cardG_gt0 -subn1 subn_gt0 prime_gt1.
-have{nH1U cycUhat} a_dv_u: a %| u.
-  rewrite /u card_quotient ?normal_norm // indexgS // defU'.
-  rewrite der1_min ?cyclic_abelian // normsI ?normG //.
-  by rewrite (subset_trans nH1U) // astab_norm.
-pose j := j1; pose psi := mu_ j - (u %/ a)%:R *: lambda.
-have /andP/=[red_muj S2muj]: mu_ j \in [predD S2 & irr M].
-  by rewrite memS2red image_f.
-have S2psi: psi \in 'Z[S2, M^#].
-  rewrite zcharD1E rpredB ?rpredZnat ?mem_zchar //=.
-  by rewrite !cfunE mu_1 // lambda1 -natrM mulnCA divnK ?subrr.
-pose phi := tau (mu_ 0 - zeta).
-have o_phi_psi: '[phi, tau psi] = 0.
-  have Apsi: psi \in 'CF(M, 'A(M)) by rewrite defA (zcharD1_seqInd_on _ S2psi).
-  have [Tzeta Tlambda] := (seqInd_subT  S1zeta, seqInd_subT S2lambda).
-  rewrite Dade_isometry ?A0bridge0 ?(cfun_onS (FTsupp_sub0 M)) //.
-  rewrite cfdotBl !cfdotBr !cfdotZr cfdot_prTIred eq_sym (negPf nz_j1) add0r.
-  rewrite !(seqInd_ortho _ Tzeta) ?Tmu ?(memPnC (sS1S2' S1zeta)) // add0r.
-  rewrite (seqInd_ortho _ (Tmu 0)) ?(memPnC (prTIred_not_irr _ _)) // !mulr0.
-  by rewrite subrr.
-have [tau2 coh_tau2] := cohS2; have [[_ Ztau2] Dtau2] := coh_tau2.
-have ua_1: (u %/ a)%:R * `|'[phi, tau2 lambda]| == 1.
-  rewrite -normr_nat -normrM mulr_natl -!raddfMn -[_ *+ _](subrK (mu_ j)) /=.
-  rewrite -opprB addrC raddfB cfdotBr -scaler_nat (Dtau2 _ S2psi) o_phi_psi.
-  case: (FTtypeP_coherent_TIred _ coh_tau2 _ S2lambda S2muj) => // -[b k] -> _.
-  rewrite -/(eta_col k) cfdotZr rmorph_sign subr0 normrMsign.
-  rewrite -[phi](subrK eta0row) cfdotDl cfdot_sumr big1 => [|j' _]; last first.
-    by rewrite (orthoPl (bridgeS1 _ _)) ?map_f ?mem_irr.
-  rewrite add0r cfdotC norm_conjC cfdot_sumr (bigD1 k) //= proj_col_eta eqxx.
-  by rewrite big1 ?addr0 ?normr1 // => i k'i; rewrite proj_col_eta (negPf k'i).
-have Du: u = a.
-  apply/eqP; rewrite -[a]mul1n eqn_mul ?(ltnW a_gt1) // -eqC_nat.
-  move: ua_1; rewrite Cnat_mul_eq1 ?rpred_nat //; first by case/andP.
-  rewrite Cnat_norm_Cint ?Cint_cfdot_vchar //; last by rewrite Ztau2 ?mem_zchar.
-  rewrite Dade_vchar // zchar_split A0bridge0 //.
-  by rewrite rpredB ?char_vchar ?prTIred_char ?irrWchar.
-have lequ: (q <= u)%N.
-  have u1_gt0: (0 < u.-1)%N by rewrite -subn1 subn_gt0 Du.
-  rewrite (leq_trans _ (leq_pred u)) // dvdn_leq //.
-  suffices ->: q = #|W1 / C|%g by apply: Frobenius_dvd_ker1 frobUW1bar.
-  apply/card_isog/quotient_isog; first by have [] := joing_subP nC_UW1.
-  by rewrite setIAC (coprime_TIg coUq) setI1g.
-by rewrite (leq_trans lequ) // Du dvdn_leq // -subn1 subn_gt0 prime_gt1.
-Qed.
-
-End Eleven.