proposition: Corollary mem_coherent_sum_subseq S1 chi (tau1 : {additive 'CF(L) -> 'CF(G)}) : cfConjC_subset S1 S -> coherent_with S1 L^# tau tau1 -> chi \in S1 -> exists2 E, subseq E (R chi) & tau1 chi = \sum_(a <- E) a.
proof: Proof. move=> uccS1 [Itau1 Dtau1] S1chi; have [uS1 sS1S ccS1] := uccS1. have S1chi_s: chi^*%CF \in S1 by apply: ccS1. apply: coherent_sum_subseq; first exact: sS1S. by apply: sub_iso_to Itau1 => //; apply: zchar_subset; apply/allP/and3P. apply: Dtau1; rewrite sub_aut_zchar ?zchar_onG ?mem_zchar // => phi /sS1S-Sphi. by apply: char_vchar; have [[->]] := cohS. 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)