move odd_order to its own repository

1 files changed, 0 insertions, 994 deletions

diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v
deleted file mode 100644
index 3cdff96..0000000
--- a/mathcomp/odd_order/PFsection4.v
+++ /dev/null
@@ -1,994 +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 fingroup.
-From mathcomp
-Require Import morphism perm automorphism quotient action gfunctor gproduct.
-From mathcomp
-Require Import center commutator zmodp cyclic pgroup nilpotent hall frobenius.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation vector ssrnum algC classfun.
-From mathcomp
-Require Import character inertia vcharacter PFsection1 PFsection2 PFsection3.
-
-(******************************************************************************)
-(* This file covers Peterfalvi, Section 4: The Dade isometry of a certain     *)
-(* type of subgroup.                                                          *)
-(*   Given defW : W1 \x W2 = W, we define here:                               *)
-(*  primeTI_hypothesis L K defW <->                                           *)
-(*                   L = K ><| W1, where W1 acts in a prime manner on K (see  *)
-(*                   semiprime in frobenius.v), and both W1 and W2 = 'C_K(W1) *)
-(*                   are nontrivial and cyclic of odd order; these conditions *)
-(*                   imply that cyclicTI_hypothesis L defW holds.             *)
-(*  -> This is Peterfalvi, Hypothesis (4.2), or Feit-Thompson (13.2).         *)
-(*  prime_Dade_definition L K H A A0 defW <->                                 *)
-(*                   A0 = A :|: class_support (cyclicTIset defW) L where A is *)
-(*                   an L-invariant subset of K^# containing all the elements *)
-(*                   of K that do not act freely on H <| L; in addition       *)
-(*                   W2 \subset H \subset K.                                  *)
-(*  prime_Dade_hypothesis G L K H A A0 defW <->                               *)
-(*                   The four assumptions primeTI_hypothesis L K defW,        *)
-(*                   cyclicTI_hypothesis G defW, Dade_hypothesis G L A0 and   *)
-(*                   prime_Dade_definition L K H A A0 defW hold jointly.      *)
-(*  -> This is Peterfalvi, Hypothesis (4.6), or Feit-Thompson (13.3) (except  *)
-(*     that H is not required to be nilpotent, and the "supporting groups"    *)
-(*     assumptions have been replaced by Dade hypothesis).                    *)
-(*  -> This hypothesis is one of the alternatives under which Sibley's        *)
-(*     coherence theorem holds (see PFsection6.v), and is verified by all     *)
-(*     maximal subgroups of type P in a minimal simple odd group.             *)
-(*  -> prime_Dade_hypothesis coerces to Dade_hypothesis, cyclicTI_hypothesis, *)
-(*     primeTI_hypothesis and prime_Dade_definition.                          *)
-(* For ptiW : primeTI_hypothesis L K defW we also define:                     *)
-(*  prime_cycTIhyp ptiW :: cyclicTI_hypothesis L defW (though NOT a coercion) *)
-(*  primeTIirr ptiW i j == the (unique) irreducible constituent of the image  *)
-(*   (locally) mu2_ i j    in 'CF(L) of w_ i j = cyclicTIirr defW i j under   *)
-(*                         the sigma = cyclicTIiso (prime_cycTIhyp ptiW).     *)
-(* primeTI_Iirr ptiW ij == the index of mu2_ ij.1 ij.2; indeed mu2_ i j is    *)
-(*                         just notation for 'chi_(primeTI_Iirr ptiW (i, j)). *)
-(*   primeTIsign ptiW j == the sign of mu2_ i j in sigma (w_ i j), which does *)
-(*   (locally) delta_ j    not depend on i.                                   *)
-(* primeTI_Isign ptiW j == the boolean b such that delta_ j := (-1) ^+ b.     *)
-(*    primeTIres ptiW j == the restriction to K of mu2_ i j, which is an      *)
-(*     (locally) chi_ j    irreducible character that does not depend on i.   *)
-(*  primeTI_Ires ptiW j == the index of chi_ j := 'chi_(primeTI_Ires ptiW j). *)
-(*    primeTIred ptiW j == the (reducible) character equal to the sum of all  *)
-(*      (locally) mu_ j    the mu2_ i j, and also to 'Ind (chi_ j).           *)
-(* uniform_prTIred_seq ptiW k == the sequence of all the mu_ j, j != 0, with  *)
-(*                         the same degree as mu_ k (s.t. mu_ j 1 = mu_ k 1). *)
-(******************************************************************************)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Import GroupScope GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
-
-Section Four_1_to_2.
-
-(* This is Peterfalvi (4.1). *)
-
-Variable gT : finGroupType.
-
-Lemma vchar_pairs_orthonormal (X : {group gT}) (a b c d : 'CF(X)) u v :
-    {subset (a :: b) <= 'Z[irr X]} /\ {subset (c :: d) <= 'Z[irr X]} ->
-    orthonormal (a :: b) && orthonormal (c :: d) ->
-    [&& u \is Creal, v \is Creal, u != 0 & v != 0] ->
-    [&& '[a - b, u *: c - v *: d] == 0,
-         (a - b) 1%g == 0 & (u *: c - v *: d) 1%g == 0] ->
-    orthonormal [:: a; b; c; d].
-Proof.
-have osym2 (e f : 'CF(X)) : orthonormal (e :: f) -> orthonormal (f :: e).
-  by rewrite !(orthonormal_cat [::_] [::_]) orthogonal_sym andbCA.
-have def_o f S: orthonormal (f :: S) -> '[f : 'CF(X)] = 1.
-  by case/andP=> /andP[/eqP].
-case=> /allP/and3P[Za Zb _] /allP/and3P[Zc Zd _] /andP[o_ab o_cd].
-rewrite (orthonormal_cat (a :: b)) o_ab o_cd /=.
-case/and4P=> r_u r_v nz_u nz_v /and3P[o_abcd ab1 cd1].
-wlog suff: a b c d u v Za Zb Zc Zd o_ab o_cd r_u r_v nz_u nz_v o_abcd ab1 cd1 /
-  '[a, c]_X == 0.
-- move=> IH; rewrite /orthogonal /= !andbT (IH a b c d u v) //=.
-  have vc_sym (e f : 'CF(X)) : ((e - f) 1%g == 0) = ((f - e) 1%g == 0).
-    by rewrite -opprB cfunE oppr_eq0.
-  have ab_sym e: ('[b - a, e] == 0) = ('[a - b, e] == 0).
-    by rewrite -opprB cfdotNl oppr_eq0.
-  rewrite (IH b a c d u v) // 1?osym2 1?vc_sym ?ab_sym //=.
-  rewrite -oppr_eq0 -cfdotNr opprB in o_abcd.
-  by rewrite (IH a b d c v u) ?(IH b a d c v u) // 1?osym2 1?vc_sym ?ab_sym.
-apply: contraLR cd1 => nz_ac.
-have [/orthonormal2P[ab0 a1 b1] /orthonormal2P[cd0 c1 d1]] := (o_ab, o_cd).
-have [ea [ia def_a]] := vchar_norm1P Za a1.
-have{nz_ac} [e defc]: exists e : bool, c = (-1) ^+ e *: a.
-  have [ec [ic def_c]] := vchar_norm1P Zc c1; exists (ec (+) ea).
-  move: nz_ac; rewrite def_a def_c scalerA; rewrite -signr_addb addbK.
-  rewrite cfdotZl cfdotZr cfdot_irr mulrA mulrC mulf_eq0.
-  by have [-> // | _]:= ia =P ic; rewrite eqxx.
-have def_vbd: v * '[b, d]_X = - ((-1) ^+ e * u).
-  apply/eqP; have:= o_abcd; rewrite cfdotDl cfdotNl !raddfB /=.
-  rewrite defc !cfdotZr a1 (cfdotC b) ab0 rmorph0 mulr1.
-  rewrite -[a]scale1r -{2}[1]/((-1) ^+ false) -(addbb e) signr_addb -scalerA.
-  rewrite -defc cfdotZl cd0 !mulr0 opprK addrA !subr0 mulrC addrC addr_eq0.
-  by rewrite rmorph_sign !conj_Creal.
-have nz_bd: '[b, d] != 0.
-  move/esym/eqP: def_vbd; apply: contraTneq => ->.
-  by rewrite mulr0 oppr_eq0 mulf_eq0 signr_eq0.
-have{nz_bd} defd: d = '[b, d] *: b.
-  move: nz_bd; have [eb [ib ->]] := vchar_norm1P Zb b1.
-  have [ed [id ->]] := vchar_norm1P Zd d1.
-  rewrite scalerA cfdotZl cfdotZr rmorph_sign mulrA cfdot_irr.
-  have [-> _ | _] := ib =P id; last by rewrite !mulr0 eqxx.
-  by rewrite mulr1 mulrAC -!signr_addb addbb.
-rewrite defd scalerA def_vbd scaleNr opprK defc scalerA mulrC -raddfD cfunE.
-rewrite !mulf_neq0 ?signr_eq0 // -(subrK a b) -opprB addrCA 2!cfunE.
-rewrite (eqP ab1) oppr0 add0r cfunE -mulr2n -mulr_natl mulf_eq0 pnatr_eq0.
-by rewrite /= def_a cfunE mulf_eq0 signr_eq0 /= irr1_neq0.
-Qed.
-
-Corollary orthonormal_vchar_diff_ortho (X : {group gT}) (a b c d : 'CF(X)) :
-    {subset a :: b <= 'Z[irr X]} /\ {subset c :: d <= 'Z[irr X]} ->
-    orthonormal (a :: b) && orthonormal (c :: d) ->
-    [&& '[a - b, c - d] == 0, (a - b) 1%g == 0 & (c - d) 1%g == 0] ->
-  '[a, c] = 0.
-Proof.
-move=> Zabcd Oabcd; rewrite -[c - d]scale1r scalerBr.
-move/(vchar_pairs_orthonormal Zabcd Oabcd) => /implyP.
-rewrite rpred1 oner_eq0 (orthonormal_cat (a :: b)) /=.
-by case/and3P=> _ _ /andP[] /andP[] /eqP.
-Qed.
-
-(* This is Peterfalvi, Hypothesis (4.2), with explicit parameters. *)
-Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) of W1 \x W2 = W :=
-  [/\ (*a*) [/\ K ><| W1 = L, W1 != 1, Hall L W1 & cyclic W1],
-      (*b*) [/\ W2 != 1, W2 \subset K & cyclic W2],
-            {in W1^#, forall x, 'C_K[x] = W2}
-   &  (*c*) odd #|W|]%g.
-
-End Four_1_to_2.
-
-Arguments primeTI_hypothesis _ _%g _%g _%g _ _%g _%g.
-
-Section Four_3_to_5.
-
-Variables (gT : finGroupType) (L K W W1 W2 : {group gT}) (defW : W1 \x W2 = W).
-Hypothesis ptiWL : primeTI_hypothesis L K defW.
-
-Let V := cyclicTIset defW.
-Let w1 := #|W1|.
-Let w2 := #|W2|.
-
-Let defL : K ><| W1 = L. Proof. by have [[]] := ptiWL. Qed.
-Let ntW1 : W1 :!=: 1%g. Proof. by have [[]] := ptiWL. Qed.
-Let cycW1 : cyclic W1. Proof. by have [[]] := ptiWL. Qed.
-Let hallW1 : Hall L W1. Proof. by have [[]] := ptiWL. Qed.
-
-Let ntW2 : W2 :!=: 1%g. Proof. by have [_ []] := ptiWL. Qed.
-Let sW2K : W2 \subset K. Proof. by have [_ []] := ptiWL. Qed.
-Let cycW2 : cyclic W2. Proof. by have [_ []] := ptiWL. Qed.
-Let prKW1 : {in W1^#, forall x, 'C_K[x] = W2}. Proof. by have [] := ptiWL. Qed.
-
-Let oddW : odd #|W|. Proof. by have [] := ptiWL. Qed.
-
-Let nsKL : K <| L. Proof. by case/sdprod_context: defL. Qed.
-Let sKL : K \subset L. Proof. by case/andP: nsKL. Qed.
-Let sW1L : W1 \subset L. Proof. by case/sdprod_context: defL. Qed.
-Let sWL : W \subset L.
-Proof. by rewrite -(dprodWC defW) -(sdprodW defL) mulgSS. Qed.
-Let sW1W : W1 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.
-Let sW2W : W2 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.
-
-Let coKW1 : coprime #|K| #|W1|.
-Proof. by rewrite (coprime_sdprod_Hall_r defL). Qed.
-Let coW12 : coprime #|W1| #|W2|.
-Proof. by rewrite coprime_sym (coprimeSg sW2K). Qed.
-
-Let cycW : cyclic W. Proof. by rewrite (cyclic_dprod defW). Qed.
-Let cWW : abelian W. Proof. exact: cyclic_abelian. Qed.
-Let oddW1 : odd w1. Proof. exact: oddSg oddW. Qed.
-Let oddW2 : odd w2. Proof. exact: oddSg oddW. Qed.
-
-Let ntV : V != set0.
-Proof.
-by rewrite -card_gt0 card_cycTIset muln_gt0 -!subn1 !subn_gt0 !cardG_gt1 ntW1.
-Qed.
-
-Let sV_V2 : V \subset W :\: W2. Proof. by rewrite setDS ?subsetUr. Qed.
-
-Lemma primeTIhyp_quotient (M : {group gT}) :
-    (W2 / M != 1)%g -> M \subset K -> M <| L ->
-  {defWbar : (W1 / M) \x (W2 / M) = W / M
-           & primeTI_hypothesis (L / M) (K / M) defWbar}%g.
-Proof.
-move=> ntW2bar sMK /andP[_ nML].
-have coMW1: coprime #|M| #|W1| by rewrite (coprimeSg sMK).
-have [nMW1 nMW] := (subset_trans sW1L nML, subset_trans sWL nML).
-have defWbar: (W1 / M) \x (W2 / M) = (W / M)%g.
-  by rewrite (quotient_coprime_dprod nMW) ?quotient_odd.
-exists defWbar; split; rewrite ?quotient_odd ?quotient_cyclic ?quotientS //.
-  have isoW1: W1 \isog W1 / M by rewrite quotient_isog ?coprime_TIg.
-  by rewrite -(isog_eq1 isoW1) ?morphim_Hall // (quotient_coprime_sdprod nML).
-move=> Kx /setD1P[ntKx /morphimP[x nKx W1x defKx]] /=.
-rewrite -cent_cycle -cycle_eq1 {Kx}defKx -quotient_cycle // in ntKx *.
-rewrite -strongest_coprime_quotient_cent ?cycle_subG //; first 1 last.
-- by rewrite subIset ?sMK.
-- by rewrite (coprimeSg (subsetIl M _)) // (coprimegS _ coMW1) ?cycle_subG.
-- by rewrite orbC abelian_sol ?cycle_abelian.
-rewrite cent_cycle prKW1 // !inE W1x (contraNneq _ ntKx) // => ->.
-by rewrite cycle1 quotient1.
-Qed.
-
-(* This is the first part of PeterFalvi, Theorem (4.3)(a). *)
-Theorem normedTI_prTIset : normedTI (W :\: W2) L W.
-Proof.
-have [[_ _ cW12 _] [_ _ nKW1 tiKW1]] := (dprodP defW, sdprodP defL).
-have nV2W: W \subset 'N(W :\: W2) by rewrite sub_abelian_norm ?subsetDl.
-have piW1_W: {in W1 & W2, forall x y, (x * y).`_\pi(W1) = x}.
-  move=> x y W1x W2y /=; rewrite consttM /commute ?(centsP cW12 y) //.
-  rewrite constt_p_elt ?(mem_p_elt _ W1x) ?pgroup_pi // (constt1P _) ?mulg1 //.
-  by rewrite /p_elt -coprime_pi' // (coprimegS _ coW12) ?cycle_subG.
-have nzV2W: W :\: W2 != set0 by apply: contraNneq ntV; rewrite -subset0 => <-.
-apply/normedTI_memJ_P; split=> // xy g V2xy Lg.
-apply/idP/idP=> [| /(subsetP nV2W)/memJ_norm->//].
-have{xy V2xy} [/(mem_dprod defW)[x [y [W1x W2y -> _]]] W2'xy] := setDP V2xy.
-have{W2'xy} ntx: x != 1%g by have:= W2'xy; rewrite groupMr // => /group1_contra.
-have{g Lg} [k [w [Kk /(subsetP sW1W)Ww -> _]]] := mem_sdprod defL Lg.
-rewrite conjgM memJ_norm ?(subsetP nV2W) ?(groupMr k) // => /setDP[Wxyk _].
-have{Wxyk piW1_W} W1xk: x ^ k \in W1.
-  have [xk [yk [W1xk W2yk Dxyk _]]] := mem_dprod defW Wxyk.
-  by rewrite -(piW1_W x y) // -consttJ Dxyk piW1_W.
-rewrite (subsetP sW2W) // -(@prKW1 x) ?in_setD1 ?ntx // inE Kk /=.
-rewrite cent1C (sameP cent1P commgP) -in_set1 -set1gE -tiKW1 inE.
-by rewrite (subsetP _ _ (mem_commg W1x Kk)) ?commg_subr // groupM ?groupV.
-Qed.
-
-(* Second part of PeterFalvi, Theorem (4.3)(a). *)
-Theorem prime_cycTIhyp : cyclicTI_hypothesis L defW.
-Proof.
-have nVW: W \subset 'N(V) by rewrite sub_abelian_norm ?subsetDl.
-by split=> //; apply: normedTI_S normedTI_prTIset.
-Qed.
-Local Notation ctiW := prime_cycTIhyp.
-Let sigma := cyclicTIiso ctiW.
-Let w_ i j := cyclicTIirr defW i j.
-
-Let Wlin k : 'chi[W]_k \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
-Let W1lin i : 'chi[W1]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
-Let W2lin i : 'chi[W2]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
-Let w_lin i j : w_ i j \is a linear_char. Proof. exact: Wlin. Qed.
-
-Let nirrW1 : #|Iirr W1| = w1. Proof. exact: card_Iirr_cyclic. Qed.
-Let nirrW2 : #|Iirr W2| = w2. Proof. exact: card_Iirr_cyclic. Qed.
-Let NirrW1 : Nirr W1 = w1. Proof. by rewrite -nirrW1 card_ord. Qed.
-Let NirrW2 : Nirr W2 = w2. Proof. by rewrite -nirrW2 card_ord. Qed.
-Let w1gt1 : (1 < w1)%N. Proof. by rewrite cardG_gt1. Qed.
-
-Let cfdot_w i1 j1 i2 j2 : '[w_ i1 j1, w_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.
-Proof. exact: cfdot_dprod_irr. Qed.
-
-(* Witnesses for Theorem (4.3)(b). *)
-Fact primeTIdIirr_key : unit. Proof. by []. Qed.
-Definition primeTIdIirr_def := dirr_dIirr (sigma \o prod_curry w_).
-Definition primeTIdIirr := locked_with primeTIdIirr_key primeTIdIirr_def.
-Definition primeTI_Iirr ij := (primeTIdIirr ij).2.
-Definition primeTI_Isign j := (primeTIdIirr (0, j)).1.
-Local Notation Imu2 := primeTI_Iirr.
-Local Notation mu2_ i j := 'chi_(primeTI_Iirr (i, j)).
-Local Notation delta_ j := (GRing.sign algCring (primeTI_Isign j)).
-
-Let ew_ i j := w_ i j - w_ 0 j.
-Let V2ew i j : ew_ i j \in 'CF(W, W :\: W2).
-Proof.
-apply/cfun_onP=> x; rewrite !inE negb_and negbK => /orP[W2x | /cfun0->//].
-by rewrite -[x]mul1g !cfunE /w_ !dprod_IirrE !cfDprodE ?lin_char1 ?subrr.
-Qed.
-
-(* This is Peterfalvi, Theorem (4.3)(b, c). *)
-Theorem primeTIirr_spec :
- [/\ (*b*) injective Imu2,
-           forall i j, 'Ind (ew_ i j) = delta_ j *: (mu2_ i j - mu2_ 0 j),
-           forall i j, sigma (w_ i j) = delta_ j *: mu2_ i j,
-     (*c*) forall i j, {in W :\: W2, mu2_ i j =1 delta_ j *: w_ i j}
-         & forall k, k \notin codom Imu2 -> {in W :\: W2, 'chi_k =1 \0}].
-Proof.
-have isoV2 := normedTI_isometry normedTI_prTIset (setDSS sWL (sub1G W2)).
-have /fin_all_exists2[dmu injl_mu Ddmu] j:
-  exists2 dmu : bool * {ffun Iirr W1 -> Iirr L}, injective dmu.2
-    & forall i, 'Ind (ew_ i j) = dchi (dmu.1, dmu.2 i) - dchi (dmu.1, dmu.2 0).
-- pose Sj := [tuple w_ i j | i < Nirr W1].
-  have Sj0: Sj`_0 = w_ 0 j by rewrite (nth_mktuple _ 0 0).
-  have irrSj: {subset Sj <= irr W} by move=> ? /mapP[i _ ->]; apply: mem_irr.
-  have: {in 'Z[Sj, W :\: W2], isometry 'Ind, to 'Z[irr L, L^#]}.
-    split=> [|phi]; first by apply: sub_in2 isoV2; apply: zchar_on.
-    move/(zchar_subset irrSj)/(zchar_onS (setDS W (sub1G W2))).
-    by rewrite !zcharD1E cfInd1 // mulf_eq0 orbC => /andP[/cfInd_vchar-> // ->].
-  case/vchar_isometry_base=> // [|||i|mu Umu [d Ddmu]]; first by rewrite NirrW1.
-  + rewrite orthonormal_free // (sub_orthonormal irrSj) ?irr_orthonormal //.
-    by apply/injectiveP=> i1 i2 /irr_inj/dprod_Iirr_inj[].
-  + by move=> _ /mapP[i _ ->]; rewrite Sj0 !lin_char1.
-  + by rewrite nth_mktuple Sj0 V2ew.
-  exists (d, [ffun i => tnth mu i]) => [|i].
-    apply/injectiveP; congr (uniq _): Umu.
-    by rewrite (eq_map (ffunE _)) map_tnth_enum.
-  by rewrite -scalerBr /= !ffunE !(tnth_nth 0 mu) -Ddmu nth_mktuple Sj0.
-pose Imu ij := (dmu ij.2).2 ij.1; pose mu i j := 'chi_(Imu (i, j)).
-pose d j : algC := (-1) ^+ (dmu j).1.
-have{Ddmu} Ddmu i j: 'Ind (ew_ i j) = d j *: (mu i j - mu 0 j).
-  by rewrite Ddmu scalerBr.
-have{injl_mu} inj_Imu: injective Imu.
-  move=> [i1 j1] [i2 j2]; rewrite /Imu /=; pose S i j k := mu i j :: mu k j.
-  have [-> /injl_mu-> // | j2'1 /eqP/negPf[] /=] := eqVneq j1 j2.
-  apply/(can_inj oddb)/eqP; rewrite -eqC_nat -cfdot_irr -!/(mu _ _) mulr0n.
-  have oIew_j12 i k: '['Ind[L] (ew_ i j1), 'Ind[L] (ew_ k j2)] = 0.
-    by rewrite isoV2 // cfdotBl !cfdotBr !cfdot_w (negPf j2'1) !andbF !subr0.
-  have defSd i j k: mu i j - mu k j = d j *: ('Ind (ew_ i j) - 'Ind (ew_ k j)).
-    by rewrite !Ddmu -scalerBr signrZK opprB addrA subrK.
-  have Sd1 i j k: (mu i j - mu k j) 1%g == 0.
-    by rewrite defSd !(cfunE, cfInd1) ?lin_char1 // !subrr mulr0.
-  have exS i j: {k | {subset S i j k <= 'Z[irr L]} & orthonormal (S i j k)}.
-    have:= w1gt1; rewrite -nirrW1 (cardD1 i) => /card_gt0P/sigW[k /andP[i'k _]].
-    exists k; first by apply/allP; rewrite /= !irr_vchar.
-    apply/andP; rewrite /= !cfdot_irr !eqxx !andbT /=.
-    by rewrite (inj_eq (injl_mu j)) mulrb ifN_eqC.
-  have [[k1 ZS1 o1S1] [k2 ZS2 o1S2]] := (exS i1 j1, exS i2 j2).
-  rewrite (orthonormal_vchar_diff_ortho (conj ZS1 ZS2)) ?o1S1 ?Sd1 ?andbT //.
-  by rewrite !defSd cfdotZl cfdotZr cfdotBl !cfdotBr !oIew_j12 !subrr !mulr0.
-pose V2base := [tuple of [seq ew_ ij.1 ij.2 | ij in predX (predC1 0) predT]].
-have V2basis: basis_of 'CF(W, W :\: W2) V2base.
-  suffices V2free: free V2base.
-    rewrite basisEfree V2free size_image /= cardX cardC1 nirrW1 nirrW2 -subn1.
-    rewrite mulnBl mul1n dim_cfun_on_abelian ?subsetDl //.
-    rewrite cardsD (setIidPr _) //  (dprod_card defW) leqnn andbT.
-    by apply/span_subvP=> _ /mapP[ij _ ->].
-  apply/freeP=> /= z zV2e0 k.
-  move Dk: (enum_val k) (enum_valP k) => [i j] /andP[/= nz_i _].
-  rewrite -(cfdot0l (w_ i j)) -{}zV2e0 cfdot_suml (bigD1 k) //= cfdotZl.
-  rewrite nth_image Dk cfdotBl !cfdot_w !eqxx eq_sym (negPf nz_i) subr0 mulr1.
-  rewrite big1 ?addr0 // => k1; rewrite -(inj_eq enum_val_inj) {}Dk nth_image.
-  case: (enum_val k1) => /= i1 j1 ij'ij1.
-  rewrite cfdotZl cfdotBl !cfdot_dprod_irr [_ && _](negPf ij'ij1).
-  by rewrite eq_sym (negPf nz_i) subr0 mulr0.
-have nsV2W: W :\: W2 <| W by rewrite -sub_abelian_normal ?subsetDl.
-pose muW k := let: ij := inv_dprod_Iirr defW k in d ij.2 *: mu ij.1 ij.2.
-have inW := codomP (dprod_Iirr_onto defW _).
-have ImuW k1 k2: '[muW k1, muW k2] = (k1 == k2)%:R.
-  have [[[i1 j1] -> {k1}] [[i2 j2] -> {k2}]] := (inW k1, inW k2).
-  rewrite cfdotZl cfdotZr !dprod_IirrK (can_eq (dprod_IirrK _)) /= rmorph_sign.
-  rewrite cfdot_irr (inj_eq inj_Imu (_, _) (_, _)) -/(d _).
-  by case: eqP => [[_ ->] | _]; rewrite ?signrMK ?mulr0.
-have [k|muV2 mu'V2] := equiv_restrict_compl_ortho sWL nsV2W V2basis ImuW.
-  rewrite nth_image; case: (enum_val k) (enum_valP k) => /= i j /andP[/= nzi _].
-  pose inWj i1 := dprod_Iirr defW (i1, j); rewrite (bigD1 (inWj 0)) //=.
-  rewrite (bigD1 (inWj i)) ?(can_eq (dprod_IirrK _)) ?xpair_eqE ?(negPf nzi) //.
-  rewrite /= big1 ?addr0 => [|k1 /andP[]]; last first.
-    rewrite !(eq_sym k1); have [[i1 j1] -> {k1}] := inW k1.
-    rewrite !(can_eq (dprod_IirrK _)) => ij1'i ij1'0.
-    by rewrite cfdotBl !cfdot_w !mulrb !ifN // subrr scale0r.
-  rewrite /muW !dprod_IirrK /= addrC !cfdotBl !cfdot_w !eqxx /= !andbT.
-  by rewrite eq_sym (negPf nzi) subr0 add0r scaleNr !scale1r -scalerBr.
-have Dsigma i j: sigma (w_ i j) = d j *: mu i j.
-  apply/esym/eq_in_cycTIiso=> [|x Vx]; first exact: (dirr_dchi (_, _)).
-  by rewrite -muV2 ?(subsetP sV_V2) // /muW dprod_IirrK.
-have /all_and2[Dd Dmu] j: d j = delta_ j /\ forall i, Imu (i, j) = Imu2 (i, j).
-  suffices DprTI i: primeTIdIirr (i, j) = ((dmu j).1, (dmu j).2 i).
-    by split=> [|i]; rewrite /primeTI_Isign /Imu2 DprTI.
-  apply: dirr_inj; rewrite /primeTIdIirr unlock_with dirr_dIirrE /= ?Dsigma //.
-  by case=> i1 j1; apply: cycTIiso_dirr.
-split=> [[i1 j1] [i2 j2] | i j | i j | i j x V2x | k mu2p'k].
-- by rewrite -!Dmu => /inj_Imu.
-- by rewrite -!Dmu -Dd -Ddmu.
-- by rewrite -Dmu -Dd -Dsigma.
-- by rewrite cfunE -muV2 // /muW dprod_IirrK Dd cfunE signrMK -Dmu.
-apply: mu'V2 => k1; have [[i j] ->{k1}] := inW k1.
-apply: contraNeq mu2p'k; rewrite cfdotZr rmorph_sign mulf_eq0 signr_eq0 /=.
-rewrite /mu Dmu dprod_IirrK -irr_consttE constt_irr inE /= => /eqP <-.
-exact: codom_f.
-Qed.
-
-(* These lemmas restate the various parts of Theorem (4.3)(b, c) separately. *)
-Lemma prTIirr_inj : injective Imu2. Proof. by case: primeTIirr_spec. Qed.
-
-Corollary cfdot_prTIirr i1 j1 i2 j2 :
-  '[mu2_ i1 j1, mu2_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.
-Proof. by rewrite cfdot_irr (inj_eq prTIirr_inj). Qed.
-
-Lemma cfInd_sub_prTIirr i j :
-  'Ind[L] (w_ i j - w_ 0 j) = delta_ j *: (mu2_ i j - mu2_ 0 j).
-Proof. by case: primeTIirr_spec i j. Qed.
-
-Lemma cycTIiso_prTIirr i j : sigma (w_ i j) = delta_ j *: mu2_ i j.
-Proof. by case: primeTIirr_spec. Qed.
-
-Lemma prTIirr_id i j : {in W :\: W2, mu2_ i j =1 delta_ j *: w_ i j}.
-Proof. by case: primeTIirr_spec. Qed.
-
-Lemma not_prTIirr_vanish k : k \notin codom Imu2 -> {in W :\: W2, 'chi_k =1 \0}.
-Proof. by case: primeTIirr_spec k. Qed.
-
-(* This is Peterfalvi, Theorem (4.3)(d). *)
-Theorem prTIirr1_mod i j : (mu2_ i j 1%g == delta_ j %[mod w1])%C.
-Proof.
-rewrite -(cfRes1 W1) -['Res _](subrK ('Res (delta_ j *: w_ i j))) cfunE.
-set phi := _ - _; pose a := '[phi, 1].
-have phi_on_1: phi \in 'CF(W1, 1%g).
-  apply/cfun_onP=> g; have [W1g | /cfun0-> //] := boolP (g \in W1).
-  rewrite -(coprime_TIg coW12) inE W1g !cfunE !cfResE //= => W2'g.
-  by rewrite prTIirr_id ?cfunE ?subrr // inE W2'g (subsetP sW1W).
-have{phi_on_1} ->: phi 1%g = a * w1%:R.
-  rewrite mulrC /a (cfdotEl _ phi_on_1) mulVKf ?neq0CG //.
-  by rewrite big_set1 cfun11 conjC1 mulr1.
-rewrite cfResE // cfunE lin_char1 // mulr1 eqCmod_addl_mul //.
-by rewrite Cint_cfdot_vchar ?rpred1 ?rpredB ?cfRes_vchar ?rpredZsign ?irr_vchar.
-Qed.
-
-Lemma prTIsign_aut u j : delta_ (aut_Iirr u j) = delta_ j.
-Proof.
-have /eqP := cfAut_cycTIiso ctiW u (w_ 0 j).
-rewrite -cycTIirr_aut aut_Iirr0 -/sigma !cycTIiso_prTIirr raddfZsign /=.
-by rewrite -aut_IirrE eq_scaled_irr => /andP[/eqP].
-Qed.
-
-Lemma prTIirr_aut u i j :
-  mu2_ (aut_Iirr u i) (aut_Iirr u j) = cfAut u (mu2_ i j).
-Proof.
-rewrite -!(canLR (signrZK _) (cycTIiso_prTIirr _ _)) -!/(delta_ _).
-by rewrite prTIsign_aut raddfZsign /= cfAut_cycTIiso -cycTIirr_aut.
-Qed.
-
-(* The (reducible) column sums of the prime TI irreducibles. *)
-Definition primeTIred j : 'CF(L) := \sum_i mu2_ i j.
-Local Notation mu_ := primeTIred.
-
-Definition uniform_prTIred_seq j0 :=
-  image mu_ [pred j | j != 0 & mu_ j 1%g == mu_ j0 1%g].
-
-Lemma prTIred_aut u j : mu_ (aut_Iirr u j) = cfAut u (mu_ j).
-Proof.
-rewrite raddf_sum [mu_ _](reindex_inj (aut_Iirr_inj u)).
-by apply: eq_bigr => i _; rewrite /= prTIirr_aut.
-Qed.
-
-Lemma cfdot_prTIirr_red i j k : '[mu2_ i j, mu_ k] = (j == k)%:R.
-Proof.
-rewrite cfdot_sumr (bigD1 i) // cfdot_prTIirr eqxx /=.
-rewrite big1 ?addr0 // => i1 neq_i1i.
-by rewrite cfdot_prTIirr eq_sym (negPf neq_i1i).
-Qed.
-
-Lemma cfdot_prTIred j1 j2 : '[mu_ j1, mu_ j2] = ((j1 == j2) * w1)%:R.
-Proof.
-rewrite cfdot_suml (eq_bigr _ (fun i _ => cfdot_prTIirr_red i _ _)) sumr_const.
-by rewrite mulrnA card_Iirr_cyclic.
-Qed.
-
-Lemma cfnorm_prTIred j : '[mu_ j] = w1%:R.
-Proof. by rewrite cfdot_prTIred eqxx mul1n. Qed.
-
-Lemma prTIred_neq0 j : mu_ j != 0.
-Proof. by rewrite -cfnorm_eq0 cfnorm_prTIred neq0CG. Qed.
-
-Lemma prTIred_char j : mu_ j \is a character.
-Proof. by apply: rpred_sum => i _; apply: irr_char. Qed.
-
-Lemma prTIred_1_gt0 j : 0 < mu_ j 1%g.
-Proof. by rewrite char1_gt0 ?prTIred_neq0 ?prTIred_char. Qed.
-
-Lemma prTIred_1_neq0 i : mu_ i 1%g != 0.
-Proof. by rewrite char1_eq0 ?prTIred_neq0 ?prTIred_char. Qed.
-
-Lemma prTIred_inj : injective mu_.
-Proof.
-move=> j1 j2 /(congr1 (cfdot (mu_ j1)))/esym/eqP; rewrite !cfdot_prTIred.
-by rewrite eqC_nat eqn_pmul2r ?cardG_gt0 // eqxx; case: (j1 =P j2).
-Qed.
-
-Lemma prTIred_not_real j : j != 0 -> ~~ cfReal (mu_ j).
-Proof.
-apply: contraNneq; rewrite -prTIred_aut -irr_eq1 -odd_eq_conj_irr1 //.
-by rewrite -aut_IirrE => /prTIred_inj->.
-Qed.
-
-Lemma prTIsign0 : delta_ 0 = 1.
-Proof.
-have /esym/eqP := cycTIiso_prTIirr 0 0; rewrite -[sigma _]scale1r.
-by rewrite /w_ /sigma cycTIirr00 cycTIiso1 -irr0 eq_scaled_irr => /andP[/eqP].
-Qed.
-
-Lemma prTIirr00 : mu2_ 0 0 = 1.
-Proof.
-have:= cycTIiso_prTIirr 0 0; rewrite prTIsign0 scale1r.
-by rewrite /w_ /sigma cycTIirr00 cycTIiso1.
-Qed.
-
-(* This is PeterFalvi (4.4). *)
-Lemma prTIirr0P k :
-  reflect (exists i, 'chi_k = mu2_ i 0) (K \subset cfker 'chi_k).
-Proof.
-suff{k}: [set k | K \subset cfker 'chi_k] == [set Imu2 (i, 0) | i : Iirr W1].
-  move/eqP/setP/(_ k); rewrite inE => ->.
-  by apply: (iffP imsetP) => [[i _]|[i /irr_inj]] ->; exists i.
-have [isoW1 abW1] := (sdprod_isog defL, cyclic_abelian cycW1).
-have abLbar: abelian (L / K) by rewrite -(isog_abelian isoW1).
-rewrite eqEcard andbC card_imset ?nirrW1 => [| i1 i2 /prTIirr_inj[] //].
-rewrite [w1](card_isog isoW1) -card_Iirr_abelian //.
-rewrite -(card_image (can_inj (mod_IirrK nsKL))) subset_leq_card; last first.
-  by apply/subsetP=> _ /imageP[k1 _ ->]; rewrite inE mod_IirrE ?cfker_mod.
-apply/subsetP=> k; rewrite inE => kerKk.
-have /irrP[ij DkW]: 'Res 'chi_k \in irr W.
-  rewrite lin_char_irr ?cfRes_lin_char // lin_irr_der1.
-  by apply: subset_trans kerKk; rewrite der1_min ?normal_norm.
-have{ij DkW} [i DkW]: exists i, 'Res 'chi_k = w_ i 0.
-  have /codomP[[i j] Dij] := dprod_Iirr_onto defW ij; exists i.
-  rewrite DkW Dij; congr (w_ i _); apply/eqP; rewrite -subGcfker.
-  rewrite -['chi_j](cfDprodKr_abelian defW i) // -dprod_IirrE -{}Dij -{}DkW.
-  by rewrite cfResRes // sub_cfker_Res // (subset_trans sW2K kerKk).
-apply/imsetP; exists i => //=; apply/irr_inj.
-suffices ->: 'chi_k = delta_ 0 *: mu2_ i 0 by rewrite prTIsign0 scale1r.
-rewrite -cycTIiso_prTIirr -(eq_in_cycTIiso _ (irr_dirr k)) // => x /setDP[Wx _].
-by rewrite -/(w_ i 0) -DkW cfResE.
-Qed.
-
-(* This is the first part of PeterFalvi, Theorem (4.5)(a). *)
-Theorem cfRes_prTIirr_eq0 i j : 'Res[K] (mu2_ i j) = 'Res (mu2_ 0 j).
-Proof.
-apply/eqP; rewrite -subr_eq0 -rmorphB /=; apply/eqP/cfun_inP=> x0 Kx0.
-rewrite -(canLR (signrZK _) (cfInd_sub_prTIirr i j)) -/(delta_ j).
-rewrite cfResE // !cfunE (cfun_on0 (cfInd_on _ (V2ew i j))) ?mulr0 //.
-apply: contraL Kx0 => /imset2P[x y /setDP[Wx W2'x] Ly ->] {x0}.
-rewrite memJ_norm ?(subsetP (normal_norm nsKL)) //; apply: contra W2'x => Kx.
-by rewrite -(mul1g W2) -(coprime_TIg coKW1) group_modr // inE Kx (dprodW defW).
-Qed.
-
-Lemma prTIirr_1 i j : mu2_ i j 1%g = mu2_ 0 j 1%g.
-Proof. by rewrite -!(@cfRes1 _ K L) cfRes_prTIirr_eq0. Qed.
-
-Lemma prTIirr0_1 i : mu2_ i 0 1%g = 1.
-Proof. by rewrite prTIirr_1 prTIirr00 cfun11. Qed.
-
-Lemma prTIirr0_linear i : mu2_ i 0 \is a linear_char.
-Proof. by rewrite qualifE irr_char /= prTIirr0_1. Qed.
-
-Lemma prTIred_1 j : mu_ j 1%g = w1%:R * mu2_ 0 j 1%g.
-Proof.
-rewrite mulr_natl -nirrW1 sum_cfunE.
-by rewrite -sumr_const; apply: eq_bigr => i _; rewrite prTIirr_1.
-Qed.
-
-Definition primeTI_Ires j : Iirr K := cfIirr ('Res[K] (mu2_ 0 j)).
-Local Notation Ichi := primeTI_Ires.
-Local Notation chi_ j := 'chi_(Ichi j).
-
-(* This is the rest of PeterFalvi, Theorem (4.5)(a). *)
-Theorem prTIres_spec j : chi_ j = 'Res (mu2_ 0 j) /\ mu_ j = 'Ind (chi_ j).
-Proof.
-rewrite /Ichi; set chi_j := 'Res _.
-have [k chi_j_k]: {k | k \in irr_constt chi_j} := constt_cfRes_irr K _.
-have Nchi_j: chi_j \is a character by rewrite cfRes_char ?irr_char.
-have lb_mu_1: w1%:R * 'chi_k 1%g <= mu_ j 1%g ?= iff (chi_j == 'chi_k).
-  have [chi' Nchi' Dchi_j] := constt_charP _ Nchi_j chi_j_k.
-  rewrite prTIred_1 (mono_lerif (ler_pmul2l (gt0CG W1))).
-  rewrite -subr_eq0 Dchi_j addrC addKr -(canLR (addrK _) Dchi_j) !cfunE.
-  rewrite lerif_subLR addrC -lerif_subLR cfRes1 subrr -char1_eq0 // eq_sym.
-  by apply: lerif_eq; rewrite char1_ge0.
-pose psi := 'Ind 'chi_k - mu_ j; have Npsi: psi \is a character.
-  apply/forallP=> l; rewrite coord_cfdot cfdotBl; set a := '['Ind _, _].
-  have Na: a \in Cnat by rewrite Cnat_cfdot_char_irr ?cfInd_char ?irr_char.
-  have [[i /eqP Dl] | ] := altP (@existsP _ (fun i => 'chi_l == mu2_ i j)).
-    have [n Da] := CnatP a Na; rewrite Da cfdotC Dl cfdot_prTIirr_red.
-    rewrite rmorph_nat -natrB ?Cnat_nat // eqxx lt0n -eqC_nat -Da.
-    by rewrite -irr_consttE constt_Ind_Res Dl cfRes_prTIirr_eq0.
-  rewrite negb_exists => /forallP muj'l.
-  rewrite cfdot_suml big1 ?subr0 // => i _.
-  rewrite cfdot_irr -(inj_eq irr_inj) mulrb ifN_eqC ?muj'l //.
-have ub_mu_1: mu_ j 1%g <= 'Ind[L] 'chi_k 1%g ?= iff ('Ind 'chi_k == mu_ j).
-  rewrite -subr_eq0 -/psi (canRL (subrK _) (erefl psi)) cfunE -lerif_subLR.
-  by rewrite subrr -char1_eq0 // eq_sym; apply: lerif_eq; rewrite char1_ge0.
-have [_ /esym] := lerif_trans lb_mu_1 ub_mu_1; rewrite cfInd1 //.
-by rewrite -(index_sdprod defL) eqxx => /andP[/eqP-> /eqP <-]; rewrite irrK.
-Qed.
-
-Lemma cfRes_prTIirr i j : 'Res[K] (mu2_ i j) = chi_ j.
-Proof. by rewrite cfRes_prTIirr_eq0; case: (prTIres_spec j). Qed.
-
-Lemma cfInd_prTIres j : 'Ind[L] (chi_ j) = mu_ j.
-Proof. by have [] := prTIres_spec j. Qed.
-
-Lemma cfRes_prTIred j : 'Res[K] (mu_ j) = w1%:R *: chi_ j.
-Proof.
-rewrite -nirrW1 scaler_nat -sumr_const linear_sum /=; apply: eq_bigr => i _.
-exact: cfRes_prTIirr.
-Qed.
-
-Lemma prTIres_aut u j : chi_ (aut_Iirr u j) = cfAut u (chi_ j).
-Proof.
-by rewrite -(cfRes_prTIirr (aut_Iirr u 0)) prTIirr_aut -cfAutRes cfRes_prTIirr.
-Qed.
-
-Lemma prTIres0 : chi_ 0 = 1.
-Proof. by rewrite -(cfRes_prTIirr 0) prTIirr00 cfRes_cfun1. Qed.
-
-Lemma prTIred0 : mu_ 0 = w1%:R *: '1_K.
-Proof.
-by rewrite -cfInd_prTIres prTIres0 cfInd_cfun1 // -(index_sdprod defL).
-Qed.
-
-Lemma prTIres_inj : injective Ichi.
-Proof. by move=> j1 j2 Dj; apply: prTIred_inj; rewrite -!cfInd_prTIres Dj. Qed.
-
-(* This is the first assertion of Peterfalvi (4.5)(b). *)
-Theorem prTIres_irr_cases k (theta := 'chi_k) (phi := 'Ind theta) :
-  {j | theta = chi_ j} + {phi \in irr L /\ (forall i j, phi != mu2_ i j)}.
-Proof.
-pose imIchi := [set Ichi j | j : Iirr W2].
-have [/imsetP/sig2_eqW[j _] | imIchi'k] := boolP (k \in imIchi).
-  by rewrite /theta => ->; left; exists j.
-suffices{phi} theta_inv: 'I_L[theta] = K.
-  have irr_phi: phi \in irr L by apply: inertia_Ind_irr; rewrite ?theta_inv.
-  right; split=> // i j; apply: contraNneq imIchi'k => Dphi; apply/imsetP.
-  exists j => //; apply/eqP; rewrite -[k == _]constt_irr -(cfRes_prTIirr i).
-  by rewrite -constt_Ind_Res -/phi Dphi irr_consttE cfnorm_irr oner_eq0.
-rewrite -(sdprodW (sdprod_modl defL (sub_inertia _))); apply/mulGidPl.
-apply/subsetP=> z /setIP[W1z Itheta_z]; apply: contraR imIchi'k => K'z.
-have{K'z} [Lz ntz] := (subsetP sW1L z W1z, group1_contra K'z : z != 1%g).
-have [p p_pr p_z]: {p | prime p & p %| #[z]} by apply/pdivP; rewrite order_gt1.
-have coKp := coprime_dvdr (dvdn_trans p_z (order_dvdG W1z)) coKW1.
-wlog{p_z} p_z: z W1z Lz Itheta_z ntz / p.-elt z.
-  move/(_ z.`_p)->; rewrite ?groupX ?p_elt_constt //.
-  by rewrite (sameP eqP constt1P) /p_elt p'natE ?negbK.
-have JirrP: is_action L (@conjg_Iirr gT K); last pose Jirr := Action JirrP.
-  split=> [y k1 k2 eq_k12 | k1 y1 y2 Gy1 Gy2]; apply/irr_inj.
-    by apply/(can_inj (cfConjgK y)); rewrite -!conjg_IirrE eq_k12.
-  by rewrite !conjg_IirrE (cfConjgM _ nsKL).
-have [[_ nKL] [nKz _]] := (andP nsKL, setIdP Itheta_z).
-suffices{k theta Itheta_z} /eqP->: imIchi == 'Fix_Jirr[z].
-  by apply/afix1P/irr_inj; rewrite conjg_IirrE inertiaJ.
-rewrite eqEcard; apply/andP; split.
-  apply/subsetP=> _ /imsetP[j _ ->]; apply/afix1P/irr_inj.
-  by rewrite conjg_IirrE -(cfRes_prTIirr 0) (cfConjgRes _ _ nsKL) ?cfConjg_id.
-have ->: #|imIchi| = w2 by rewrite card_imset //; apply: prTIres_inj.
-have actsL_KK: [acts L, on classes K | 'Js \ subsetT L].
-  rewrite astabs_ract subsetIidl; apply/subsetP=> y Ly; rewrite !inE /=.
-  apply/subsetP=> _ /imsetP[x Kx ->]; rewrite !inE /= -class_rcoset.
-  by rewrite norm_rlcoset ?class_lcoset ?mem_classes ?memJ_norm ?(subsetP nKL).
-rewrite (card_afix_irr_classes Lz actsL_KK) => [|k x y Kx /=]; last first.
-  by case/imsetP=> _ /imsetP[t Kt ->] ->; rewrite conjg_IirrE cfConjgEJ ?cfunJ.
-apply: leq_trans (subset_leq_card _) (leq_imset_card (class^~ K) _).
-apply/subsetP=> _ /setIP[/imsetP[x Kx ->] /afix1P/normP nxKz].
-suffices{Kx} /pred0Pn[t /setIP[xKt czt]]: #|'C_(x ^: K)[z]| != 0%N.
-  rewrite -(class_eqP xKt); apply: mem_imset; have [y Ky Dt] := imsetP xKt.
-  by rewrite -(@prKW1 z) ?(czt, inE) ?ntz // Dt groupJ.
-have{coKp}: ~~ (p %| #|K|) by rewrite -prime_coprime // coprime_sym.
-apply: contraNneq => /(congr1 (modn^~ p))/eqP; rewrite mod0n.
-rewrite -cent_cycle -afixJ -sylow.pgroup_fix_mod ?astabsJ ?cycle_subG //.
-by move/dvdn_trans; apply; rewrite -index_cent1 dvdn_indexg.
-Qed.
-
-(* Implicit elementary converse to the above. *)
-Lemma prTIred_not_irr j : mu_ j \notin irr L.
-Proof. by rewrite irrEchar cfnorm_prTIred pnatr_eq1 gtn_eqF ?andbF. Qed.
-
-(* This is the second assertion of Peterfalvi (4.5)(b). *)
-Theorem prTIind_irr_cases ell (phi := 'chi_ell) :
-   {i : _ & {j | phi = mu2_ i j}}
-     + {k | k \notin codom Ichi & phi = 'Ind 'chi_k}.
-Proof.
-have [k] := constt_cfRes_irr K ell; rewrite -constt_Ind_Res => kLell.
-have [[j Dk] | [/irrP/sig_eqW[l1 DkL] chi'k]] := prTIres_irr_cases k.
-  have [i /=/eqP <- | mu2j'l] := pickP (fun i => mu2_ i j == phi).
-    by left; exists i, j.
-  case/eqP: kLell; rewrite Dk cfInd_prTIres cfdot_suml big1 // => i _.
-  by rewrite cfdot_irr -(inj_eq irr_inj) mu2j'l.
-right; exists k; last by move: kLell; rewrite DkL constt_irr inE => /eqP <-.
-apply/codomP=> [[j Dk]]; have/negP[] := prTIred_not_irr j.
-by rewrite -cfInd_prTIres -Dk DkL mem_irr.
-Qed.
-
-End Four_3_to_5.
-
-Notation primeTIsign ptiW j :=
-  (GRing.sign algCring (primeTI_Isign ptiW j)) (only parsing).
-Notation primeTIirr ptiW i j := 'chi_(primeTI_Iirr ptiW (i, j)) (only parsing).
-Notation primeTIres ptiW j := 'chi_(primeTI_Ires ptiW j) (only parsing).
-
-Arguments prTIirr_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
-Arguments prTIred_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
-Arguments prTIres_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
-Arguments not_prTIirr_vanish [gT L K W W1 W2 defW] ptiWL [k].
-
-Section Four_6_t0_10.
-
-Variables (gT : finGroupType) (G L K H : {group gT}) (A A0 : {set gT}).
-Variables (W W1 W2 : {group gT}) (defW : W1 \x W2 = W).
-
-Local Notation V := (cyclicTIset defW).
-
-(* These correspond to Peterfalvi, Hypothesis (4.6). *)
-Definition prime_Dade_definition :=
-  [/\ (*c*) [/\ H <| L, W2 \subset H & H \subset K],
-      (*d*) [/\ A <| L, \bigcup_(h in H^#) 'C_K[h]^# \subset A & A \subset K^#]
-    & (*e*) A0 = A :|: class_support V L].
- 
-Record prime_Dade_hypothesis : Prop := PrimeDadeHypothesis {
-  prDade_cycTI :> cyclicTI_hypothesis G defW;
-  prDade_prTI  :> primeTI_hypothesis L K defW;
-  prDade_hyp   :> Dade_hypothesis G L A0;
-  prDade_def   :> prime_Dade_definition
-}.
-
-Hypothesis prDadeHyp : prime_Dade_hypothesis.
-
-Let ctiWG : cyclicTI_hypothesis G defW := prDadeHyp.
-Let ptiWL : primeTI_hypothesis L K defW := prDadeHyp.
-Let ctiWL : cyclicTI_hypothesis L defW := prime_cycTIhyp ptiWL.
-Let ddA0 : Dade_hypothesis G L A0 := prDadeHyp.
-Local Notation ddA0def := (prDade_def prDadeHyp).
-
-Local Notation w_ i j := (cyclicTIirr defW i j).
-Local Notation sigma := (cyclicTIiso ctiWG).
-Local Notation eta_ i j := (sigma (w_ i j)).
-Local Notation mu2_ i j := (primeTIirr ptiWL i j).
-Local Notation delta_ j := (primeTIsign ptiWL j).
-Local Notation chi_ j := (primeTIres ptiWL j).
-Local Notation mu_ := (primeTIred ptiWL).
-Local Notation tau := (Dade ddA0).
-
-Let defA0 : A0 = A :|: class_support V L. Proof. by have [] := ddA0def. Qed.
-Let nsAL : A <| L. Proof. by have [_ []] := ddA0def. Qed.
-Let sAA0 : A \subset A0. Proof. by rewrite defA0 subsetUl. Qed.
-
-Let nsHL : H <| L. Proof. by have [[]] := ddA0def. Qed.
-Let sHK : H \subset K. Proof. by have [[]] := ddA0def. Qed.
-Let defL : K ><| W1 = L. Proof. by have [[]] := ptiWL. Qed.
-Let sKL : K \subset L. Proof. by have /mulG_sub[] := sdprodW defL. Qed.
-Let coKW1 : coprime #|K| #|W1|.
-Proof. by rewrite (coprime_sdprod_Hall_r defL); have [[]] := ptiWL. Qed.
-
-Let sIH_A : \bigcup_(h in H^#) 'C_K[h]^# \subset A.
-Proof. by have [_ []] := ddA0def. Qed.
-
-Let sW2H : W2 \subset H. Proof. by have [[]] := ddA0def. Qed.
-Let ntW1 : W1 :!=: 1%g. Proof. by have [[]] := ptiWL. Qed.
-Let ntW2 : W2 :!=: 1%g. Proof. by have [_ []] := ptiWL. Qed.
-
-Let oddW : odd #|W|. Proof. by have [] := ctiWL. Qed.
-Let sW1W : W1 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.
-Let sW2W : W2 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.
-Let tiW12 : W1 :&: W2 = 1%g. Proof. by have [] := dprodP defW. Qed.
-
-Let cycW : cyclic W. Proof. by have [] := ctiWG. Qed.
-Let cycW1 : cyclic W1. Proof. by have [[]] := ptiWL. Qed.
-Let cycW2 : cyclic W2. Proof. by have [_ []] := ptiWL. Qed.
-Let sLG : L \subset G. Proof. by case: ddA0. Qed.
-Let sW2K : W2 \subset K. Proof. by have [_ []] := ptiWL. Qed.
-
-Let sWL : W \subset L.
-Proof. by rewrite -(dprodWC defW) -(sdprodW defL) mulgSS. Qed.
-Let sWG : W \subset G. Proof. exact: subset_trans sWL sLG. Qed.
-
-Let oddW1 : odd #|W1|. Proof. exact: oddSg oddW. Qed.
-Let oddW2 : odd #|W2|. Proof. exact: oddSg oddW. Qed.
-
-Let w1gt1 : (2 < #|W1|)%N. Proof. by rewrite odd_gt2 ?cardG_gt1. Qed.
-Let w2gt2 : (2 < #|W2|)%N. Proof. by rewrite odd_gt2 ?cardG_gt1. Qed.
-
-Let nirrW1 : #|Iirr W1| = #|W1|. Proof. exact: card_Iirr_cyclic. Qed.
-Let nirrW2 : #|Iirr W2| = #|W2|. Proof. exact: card_Iirr_cyclic. Qed.
-Let W1lin i : 'chi[W1]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
-Let W2lin i : 'chi[W2]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
- 
-(* This is the first part of Peterfalvi (4.7). *) 
-Lemma prDade_irr_on k : 
-   ~~ (H \subset cfker 'chi[K]_k) -> 'chi_k \in 'CF(K, 1%g |: A).
-Proof.
-move=> kerH'i; apply/cfun_onP=> g; rewrite !inE => /norP[ntg A'g].
-have [Kg | /cfun0-> //] := boolP (g \in K).
-apply: irr_reg_off_ker_0 (normalS _ _ nsHL) kerH'i _ => //.
-apply/trivgP/subsetP=> h /setIP[Hh cgh]; apply: contraR A'g => nth.
-apply/(subsetP sIH_A)/bigcupP; exists h; first exact/setDP.
-by rewrite 3!inE ntg Kg cent1C.
-Qed.
-
-(* This is the second part of Peterfalvi (4.7). *) 
-Lemma prDade_Ind_irr_on k : 
-   ~~ (H \subset cfker 'chi[K]_k) -> 'Ind[L] 'chi_k \in 'CF(L, 1%g |: A).
-Proof.
-move/prDade_irr_on/(cfInd_on sKL); apply: cfun_onS; rewrite class_supportEr.
-by apply/bigcupsP=> _ /normsP-> //; rewrite normsU ?norms1 ?normal_norm.
-Qed.
-
-(* Third part of Peterfalvi (4.7). *)
-Lemma cfker_prTIres j : j != 0 ->  ~~ (H \subset cfker (chi_ j)).
-Proof.
-rewrite -(cfRes_prTIirr _ 0) cfker_Res ?irr_char // subsetI sHK /=.
-apply: contra => kerHmu0j; rewrite -irr_eq1; apply/eqP/cfun_inP=> y W2y.
-have [[x W1x ntx] mulW] := (trivgPn _ ntW1, dprodW defW).
-rewrite cfun1E W2y -(cfDprodEr defW _ W1x W2y) -dprodr_IirrE -dprod_Iirr0l.
-have{ntx} W2'x: x \notin W2 by rewrite -[x \in W2]andTb -W1x -in_setI tiW12 inE.
-have V2xy: (x * y)%g \in W :\: W2 by rewrite inE -mulW mem_mulg ?groupMr ?W2'x.
-rewrite -[w_ 0 j](signrZK (primeTI_Isign ptiWL j)) cfunE -prTIirr_id //.
-have V2x: x \in W :\: W2 by rewrite inE W2'x (subsetP sW1W).
-rewrite cfkerMr ?(subsetP (subset_trans sW2H kerHmu0j)) ?prTIirr_id // cfunE.
-by rewrite signrMK -[x]mulg1 dprod_Iirr0l dprodr_IirrE cfDprodEr ?lin_char1.
-Qed.
-
-(* Fourth part of Peterfalvi (4.7). *)
-Lemma prDade_TIres_on j : j != 0 -> chi_ j \in 'CF(K, 1%g |: A).
-Proof. by move/cfker_prTIres/prDade_irr_on. Qed.
-
-(* Last part of Peterfalvi (4.7). *)
-Lemma prDade_TIred_on j : j != 0 -> mu_ j \in 'CF(L, 1%g |: A).
-Proof. by move/cfker_prTIres/prDade_Ind_irr_on; rewrite cfInd_prTIres. Qed.
-
-Import ssrint.
-
-(* Second part of PeterFalvi (4.8). *)
-Lemma prDade_TIsign_eq i j k : 
-  mu2_ i j 1%g = mu2_ i k 1%g -> delta_ j = delta_ k.
-Proof.
-move=> eqjk; have{eqjk}: (delta_ j == delta_ k %[mod #|W1|])%C.
-  apply: eqCmod_trans (prTIirr1_mod ptiWL i k).
-  by rewrite eqCmod_sym -eqjk (prTIirr1_mod ptiWL).
-have /negP: ~~ (#|W1| %| 2) by rewrite gtnNdvd.
-rewrite /eqCmod -![delta_ _]intr_sign -rmorphB dvdC_int ?Cint_int //= intCK.
-by do 2!case: (primeTI_Isign _ _).
-Qed.
-
-(* First part of PeterFalvi (4.8). *)
-Lemma prDade_sub_TIirr_on i j k :
-    j != 0 -> k != 0 -> mu2_ i j 1%g = mu2_ i k 1%g ->
-  mu2_ i j - mu2_ i k \in 'CF(L, A0).
-Proof.
-move=> nzj nzk eq_mu1.
-apply/cfun_onP=> g; rewrite defA0 !inE negb_or !cfunE => /andP[A'g V'g].
-have [Lg | L'g] := boolP (g \in L); last by rewrite !cfun0 ?subrr.
-have{Lg} /bigcupP[_ /rcosetsP[x W1x ->] Kx_g]: g \in cover (rcosets K W1).
-  by rewrite (cover_partition (rcosets_partition_mul W1 K)) (sdprodW defL).
-have [x1 | ntx] := eqVneq x 1%g.
-  have [-> | ntg] := eqVneq g 1%g; first by rewrite eq_mu1 subrr.
-  have{A'g} A1'g: g \notin 1%g |: A by rewrite !inE negb_or ntg.
-  rewrite x1 mulg1 in Kx_g; rewrite -!(cfResE (mu2_ i _) sKL) ?cfRes_prTIirr //.
-  by rewrite !(cfun_onP (prDade_TIres_on _)) ?subrr.
-have coKx: coprime #|K| #[x] by rewrite (coprime_dvdr (order_dvdG W1x)).
-have nKx: x \in 'N(K) by have [_ _ /subsetP->] := sdprodP defL.
-have [/cover_partition defKx _] := partition_cent_rcoset nKx coKx.
-have def_cKx: 'C_K[x] = W2 by have [_ _ -> //] := ptiWL; rewrite !inE ntx.
-move: Kx_g; rewrite -defKx def_cKx cover_imset => /bigcupP[z /(subsetP sKL)Lz].
-case/imsetP=> _ /rcosetP[y W2y ->] Dg; rewrite Dg !cfunJ //.
-have V2yx: (y * x)%g \in W :\: W2.
-  rewrite inE -(dprodWC defW) mem_mulg // andbT groupMl //.
-  by rewrite -[x \in W2]andTb -W1x -in_setI tiW12 inE.
-rewrite 2?{1}prTIirr_id //.
-have /set1P->: y \in [1].
-  rewrite -tiW12 inE W2y andbT; apply: contraR V'g => W1'y.
-  by rewrite Dg mem_imset2 // !inE negb_or -andbA -in_setD groupMr ?W1'y.
-rewrite -commute1 (prDade_TIsign_eq eq_mu1) !cfunE -mulrBr.
-by rewrite !dprod_IirrE !cfDprodE // !lin_char1 // subrr mulr0.
-Qed.
-
-(* This is last part of PeterFalvi (4.8). *)
-Lemma prDade_sub_TIirr i j k :
-    j != 0 -> k != 0 -> mu2_ i j 1%g = mu2_ i k 1%g -> 
-  tau (mu2_ i j - mu2_ i k) = delta_ j *: (eta_ i j - eta_ i k).
-Proof.
-move=> nz_j nz_k eq_mu2jk_1.
-have [-> | k'j] := eqVneq j k; first by rewrite !subrr !raddf0.
-have [[Itau Ztau] [_ Zsigma]] := (Dade_Zisometry ddA0, cycTI_Zisometry ctiWL).
-set dmu2 := _ - _; set dsw := _ - _; have Dmu2 := prTIirr_id ptiWL.
-have Zmu2: dmu2 \in 'Z[irr L, A0].
-  by rewrite zchar_split rpredB ?irr_vchar ?prDade_sub_TIirr_on.
-apply: eq_signed_sub_cTIiso => // [||x Vx].
-- exact: zcharW (Ztau _ Zmu2).
-- rewrite Itau // cfnormBd ?cfnorm_irr // (cfdot_prTIirr ptiWL).
-  by rewrite (negPf k'j) andbF.
-have V2x: x \in W :\: W2 by rewrite (subsetP _ x Vx) // setDS ?subsetUr.
-rewrite !(cfunE, Dade_id) ?(cycTIiso_restrict _ _ Vx) //; last first.
-  by rewrite defA0 inE orbC mem_class_support.
-by rewrite !Dmu2 // (prDade_TIsign_eq eq_mu2jk_1) !cfunE -mulrBr.
-Qed.
-
-Lemma prDade_supp_disjoint : V \subset ~: K.
-Proof.
-rewrite subDset setUC -subDset setDE setCK setIC -(dprod_modr defW sW2K).
-by rewrite coprime_TIg // dprod1g subsetUr.
-Qed.
-
-(* This is Peterfalvi (4.9).                                                  *)
-(* We have added the "obvious" fact that calT is pairwise orthogonal, since   *)
-(* we require this to prove membership in 'Z[calT], we encapsulate the        *)
-(* construction of tau1, and state its conformance to tau on the "larger"     *)
-(* domain 'Z[calT, L^#], so that clients can avoid using the domain equation  *)
-(* in part (a).                                                               *)
-Theorem uniform_prTIred_coherent k (calT := uniform_prTIred_seq ptiWL k) :
-    k != 0 ->
-  (*a*) [/\ pairwise_orthogonal calT, ~~ has cfReal calT, cfConjC_closed calT,
-            'Z[calT, L^#] =i 'Z[calT, A]
-          & exists2 psi, psi != 0 & psi \in 'Z[calT, A]]
-  (*b*) /\ (exists2 tau1 : {linear 'CF(L) -> 'CF(G)},
-           forall j, tau1 (mu_ j) = delta_ k *: (\sum_i sigma (w_ i j))
-         & {in 'Z[calT], isometry tau1, to 'Z[irr G]}
-        /\ {in 'Z[calT, L^#], tau1 =1 tau}).
-Proof.
-have uniqT: uniq calT by apply/dinjectiveP; apply: in2W; apply: prTIred_inj.
-have sTmu: {subset calT <= codom mu_} by apply: image_codom.
-have oo_mu: pairwise_orthogonal (codom mu_).
-  apply/pairwise_orthogonalP; split=> [|_ _ /codomP[j1 ->] /codomP[j2 ->]].
-    apply/andP; split; last by apply/injectiveP; apply: prTIred_inj.
-    by apply/codomP=> [[i /esym/eqP/idPn[]]]; apply: prTIred_neq0.
-  by rewrite cfdot_prTIred; case: (j1 =P j2) => // -> /eqP.
-have real'T: ~~ has cfReal calT.
-  by apply/hasPn=> _ /imageP[j /andP[nzj _] ->]; apply: prTIred_not_real.
-have ccT: cfConjC_closed calT.
-  move=> _ /imageP[j Tj ->]; rewrite -prTIred_aut image_f // inE aut_Iirr_eq0.
-  by rewrite prTIred_aut cfunE conj_Cnat ?Cnat_char1 ?prTIred_char.
-have TonA: 'Z[calT, L^#] =i 'Z[calT, A].
-  have A'1: 1%g \notin A by apply: contra (subsetP sAA0 _) _; have [] := ddA0.
-  move=> psi; rewrite zcharD1E -(setU1K A'1) zcharD1; congr (_ && _).
-  apply/idP/idP; [apply: zchar_trans_on psi => psi Tpsi | exact: zcharW].
-  have [j /andP[nz_j _] Dpsi] := imageP Tpsi.
-  by rewrite zchar_split mem_zchar // Dpsi prDade_TIred_on.
-move=> nzk; split.
-  split=> //; first exact: sub_pairwise_orthogonal oo_mu.
-  have Tmuk: mu_ k \in calT by rewrite image_f // inE nzk /=.
-  exists ((mu_ k)^*%CF - mu_ k); first by rewrite subr_eq0 (hasPn real'T).
-  rewrite -TonA -rpredN opprB sub_aut_zchar ?zchar_onG ?mem_zchar ?ccT //.
-  by move=> _ /mapP[j _ ->]; rewrite char_vchar ?prTIred_char.
-pose f0 j := delta_ k *: (\sum_i eta_ i j); have in_mu := codom_f mu_.
-pose f1 psi := f0 (iinv (valP (insigd (in_mu k) psi))).
-have f1mu j: f1 (mu_ j) = f0 j.
-  have in_muj := in_mu j.
-  rewrite /f1 /insigd /insubd /= insubT /=; [idtac].
-  by rewrite iinv_f //; apply: prTIred_inj.
-have iso_f1: {in codom mu_, isometry f1, to 'Z[irr G]}.
-  split=> [_ _ /codomP[j1 ->] /codomP[j2 ->] | _ /codomP[j ->]]; last first.
-    by rewrite f1mu rpredZsign rpred_sum // => i _; apply: cycTIiso_vchar.
-  rewrite !f1mu cfdotZl cfdotZr rmorph_sign signrMK !cfdot_suml.
-  apply: eq_bigr => i1 _; rewrite !cfdot_sumr; apply: eq_bigr => i2 _.
-  by rewrite cfdot_cycTIiso cfdot_prTIirr.
-have [tau1 Dtau1 Itau1] := Zisometry_of_iso (orthogonal_free oo_mu) iso_f1.
-exists tau1 => [j|]; first by rewrite Dtau1 ?codom_f ?f1mu.
-split=> [|psi]; first by apply: sub_iso_to Itau1 => //; apply: zchar_subset.
-rewrite zcharD1E => /andP[/zchar_expansion[//|z _ Dpsi] /eqP psi1_0].
-rewrite -[psi]subr0 -(scale0r (mu_ k)) -(mul0r (mu_ k 1%g)^-1) -{}psi1_0.
-rewrite {psi}Dpsi sum_cfunE mulr_suml scaler_suml -sumrB !raddf_sum /=.
-apply: eq_big_seq => _ /imageP[j /andP[nzj /eqP eq_mujk_1] ->].
-rewrite cfunE eq_mujk_1 mulfK ?prTIred_1_neq0 // -scalerBr !linearZ /=.
-congr (_ *: _); rewrite {z}linearB !Dtau1 ?codom_f // !f1mu -scalerBr -!sumrB.
-rewrite !linear_sum; apply: eq_bigr => i _ /=.
-have{eq_mujk_1} eq_mu2ijk_1: mu2_ i j 1%g = mu2_ i k 1%g.
-  by apply: (mulfI (neq0CG W1)); rewrite !prTIirr_1 -!prTIred_1.
-by rewrite -(prDade_TIsign_eq eq_mu2ijk_1) prDade_sub_TIirr.
-Qed.
-
-(* This is Peterfalvi (4.10). *)
-Lemma prDade_sub2_TIirr i j :
-  tau (delta_ j *: mu2_ i j - delta_ j *: mu2_ 0 j - mu2_ i 0 + mu2_ 0 0)
-    = eta_ i j - eta_ 0 j - eta_ i 0 + eta_ 0 0.
-Proof.
-pose V0 := class_support V L; have sVV0: V \subset V0 := sub_class_support L V.
-have sV0A0: V0 \subset A0 by rewrite defA0 subsetUr.
-have nV0L: L \subset 'N(V0) := class_support_norm V L.
-have [_ _ /normedTI_memJ_P[ntV _ tiV]] := ctiWG.
-have [/andP[sA0L _] _ A0'1 _ _] := ddA0.
-have{sA0L A0'1} sV0G: V0 \subset G^#.
-  by rewrite (subset_trans sV0A0) // subsetD1 A0'1 (subset_trans sA0L).
-have{sVV0} ntV0: V0 != set0 by apply: contraNneq ntV; rewrite -subset0 => <-.
-have{ntV} tiV0: normedTI V0 G L.
-  apply/normedTI_memJ_P; split=> // _ z /imset2P[u y Vu Ly ->] Gz.
-  apply/idP/idP=> [/imset2P[u1 y1 Vu1 Ly1 Duyz] | Lz]; last first.
-    by rewrite -conjgM mem_imset2 ?groupM.
-  rewrite -[z](mulgKV y1) groupMr // -(groupMl _ Ly) (subsetP sWL) //.
-  by rewrite -(tiV u) ?groupM ?groupV // ?(subsetP sLG) // !conjgM Duyz conjgK.
-have{ntV0 sV0A0 nV0L tiV0} DtauV0: {in 'CF(L, V0), tau =1 'Ind}.
-  by move=> beta V0beta; rewrite /= -(restr_DadeE _ sV0A0) //; apply: Dade_Ind.
-pose alpha := cfCyclicTIset defW i j; set beta := _ *: mu2_ i j - _ - _ + _.
-have Valpha: alpha \in 'CF(W, V) := cfCycTI_on ctiWL i j.
-have Dalpha: alpha = w_ i j - w_ 0 j - w_ i 0 + w_ 0 0.
-  by rewrite addrC {1}cycTIirr00 addrA addrAC addrA addrAC -cfCycTI_E.
-rewrite -!(linearB sigma) -linearD -Dalpha cycTIiso_Ind //.
-suffices ->: beta = 'Ind[L] alpha by rewrite DtauV0 ?cfInd_on ?cfIndInd.
-rewrite Dalpha -addrA -[w_ 0 0]opprK -opprD linearB /= /beta -scalerBr.
-by rewrite !(cfInd_sub_prTIirr ptiWL) prTIsign0 scale1r opprD opprK addrA.
-Qed.
- 
-End Four_6_t0_10.