proposition: Lemma FTtypeP_coherence : exists2 tau1 : {additive 'CF(S) -> 'CF(G)}, coherent_with calS S^# tau tau1 & typeP_TIred_coherent tau1.
proof: Proof. have [redS|] := altP (@allP _ [predC irr S] calS). have [k nz_k] := has_nonprincipal_irr ntW2. have [_ [tau1 Dtau1]] := uniform_prTIred_coherent pddS nz_k. set calT := uniform_prTIred_seq pddS k => cohT. exists tau1; last by exists false => // j _; rewrite /= Dtau1 delta1. apply: subset_coherent_with cohT => xi Sxi. have [_ _ /(_ xi)] := typeP_reducible_core_Ind maxS StypeP notStype5. rewrite (group_inj H0_1) mem_filter redS // => /(_ Sxi)/imageP[j nz_j ->] _. by rewrite image_f // inE -/mu_ [~~ _]nz_j /= !mu1uq. rewrite all_predC negbK => /hasP[xi Sxi irr_xi]. have [_ _ _ [tau1 cohS] _] := FTtypeP_facts; exists tau1 => //. have [|] := boolP [forall (j | j != 0), tau1 (mu_ j) == \sum_i eta_ i j]. by move/eqfun_inP=> Dtau1; exists false => // j /Dtau1; rewrite scale1r. rewrite negb_forall_in => /exists_inP[j nz_j /eqP tau1muj_neq_etaj]. have:= FTtypeP_coherent_TIred sSS0 cohS irr_xi Sxi (FTseqInd_TIred _). rewrite -/mu_ -/sigma -/ptiWS => tau1mu; have [dk tau1muj Ddk] := tau1mu j nz_j. case: Ddk tau1muj => [][-> ->]{dk}; rewrite ?signrN delta1 ?scaleNr scale1r //. set k := conjC_Iirr j => Dmu tau1muj. have{Dmu} defIW2 l: l != 0 -> pred2 j k l. by move=> nz_l; rewrite Dmu ?FTseqInd_TIred ?mu1uq. have [nz_k j'k]: k != 0 /\ k != j. rewrite conjC_Iirr_eq0 nz_j -(inj_eq irr_inj) conjC_IirrE. by rewrite odd_eq_conj_irr1 ?mFT_odd ?irr_eq1. have /eqP p3: p == 3%N. rewrite -nirrW2 (cardD1 0) (cardD1 j) (cardD1 k) !inE nz_j nz_k j'k !eqSS. by apply/pred0Pn=> [[l /and4P[k'l j'l /defIW2/norP[]]]]. exists true => // _ /defIW2/pred2P[]->; first by rewrite scaler_sign. have [[[Itau1 _] _] [d t1muk Dd]] := (cohS, tau1mu k nz_k); move: Dd t1muk. case=> [][-> ->] => [|_]; rewrite ?signrN delta1 // scale1r. case/(congr1 (cfdotr (tau1 (mu_ j)) \o -%R))/eqP/idPn => /=. rewrite -tau1muj cfdotNl eq_sym !Itau1 ?mem_zchar ?FTseqInd_TIred //. by rewrite !cfdot_prTIred (negPf j'k) eqxx mul1n oppr0 neq0CG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12)