proposition: Lemma coherent_sum_subseq chi (tau1 : {additive 'CF(L) -> 'CF(G)}) : chi \in S -> {in 'Z[chi :: chi^*%CF], isometry tau1, to 'Z[irr G]} -> tau1 (chi - chi^*%CF) = tau (chi - chi^*%CF) -> exists2 E, subseq E (R chi) & tau1 chi = \sum_(a <- E) a.
proof: Proof. set S1 := chi :: _ => Schi [iso_t1 Zt1] t1cc'. have freeS1: free S1. have [[_ nrS ccS] _ oS _ _] := cohS. by rewrite orthogonal_free ?(conjC_pair_orthogonal ccS). have subS01: {subset 'Z[chi - 0 :: chi - chi^*%CF] <= 'Z[S1]}. apply: zchar_trans setT _; apply/allP; rewrite subr0 /= andbT. by rewrite rpredB !mem_zchar ?inE ?eqxx ?orbT. have Zt1c: tau1 (chi - 0) \in 'Z[irr G]. by rewrite subr0 Zt1 ?mem_zchar ?mem_head. have [X R_X [Y defXY]] := subcoherent_split Schi Zt1c. case/subcoherent_norm: (defXY); last 2 [by []]. - by rewrite Schi rpred0 /orthogonal /= !cfdot0r eqxx. - by split; [apply: sub_in2 iso_t1 | apply: sub_in1 Zt1]. move=> _ [|_ /eqP]; rewrite cfdot0l ?cfnorm_ge0 // cfnorm_eq0 => /eqP Y0. case=> E sER defX; exists E => //; rewrite -defX -[X]subr0 -Y0 -[chi]subr0. by case: defXY. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)