proposition: Lemma FTtypeP_coherent_TIred calS1 tau1 zeta j : cfConjC_subset calS1 calS -> coherent_with calS1 M^# tau tau1 -> zeta \in irr M -> zeta \in calS1 -> mu_ j \in calS1 -> let d := primeTI_Isign ptiWM j in let k := conjC_Iirr j in {dk : bool * Iirr W2 | tau1 (mu_ j) = (-1) ^+ dk.1 *: (\sum_i eta_ i dk.2) & dk.1 = d /\ dk.2 = j \/ [/\ dk.1 = ~~ d, dk.2 = k & forall l, mu_ l \in calS1 -> mu_ l 1%g = mu_ j 1%g -> pred2 j k l]}.
proof: Proof. move=> ccsS1S cohS1 irr_zeta S1zeta S1mu_j d k. have irrS1: [/\ ~~ has cfReal calS1, has (mem (irr M)) calS1 & mu_ j \in calS1]. have [[_ -> _] _ _ _ _] := subset_subcoherent scohS ccsS1S. by split=> //; apply/hasP; exists zeta. have Dmu := coherent_prDade_TIred FT_prDade_hyp ccsS1S irrS1 cohS1. rewrite -/mu_ -/d in Dmu; pose mu_sum d1 k1 := (-1) ^+ d1 *: (\sum_i eta_ i k1). have mu_sumK (d1 d2 : bool) k1 k2: ('[mu_sum d1 k1, (-1) ^+ d2 *: eta_ 0 k2] > 0) = (d1 == d2) && (k1 == k2). - rewrite cfdotZl cfdotZr rmorph_sign mulrA -signr_addb cfdot_suml. rewrite (bigD1 0) //= cfdot_cycTIiso !eqxx big1 => [|i nz_i]; last first. by rewrite cfdot_cycTIiso (negPf nz_i). rewrite addr0 /= andbC; case: (k1 == k2); rewrite ?mulr0 ?ltrr //=. by rewrite mulr1 signr_gt0 negb_add. have [dk tau1mu_j]: {dk : bool * Iirr W2 | tau1 (mu_ j) = mu_sum dk.1 dk.2}. apply: sig_eqW; case: Dmu => [-> | [-> _]]; first by exists (d, j). by exists (~~ d, k); rewrite -signrN. exists dk => //; have:= mu_sumK dk.1 dk.1 dk.2 dk.2; rewrite !eqxx -tau1mu_j. case: Dmu => [-> | [-> all_jk]]; rewrite -?signrN mu_sumK => /andP[/eqP <- /eqP <-]; [by left | right]. by split=> // j1 S1j1 /(all_jk j1 S1j1)/pred2P. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)