proposition: Lemma coherent_seqInd_conjCirr S tau R nu r : subcoherent S tau R -> coherent_with S L^# tau nu -> let chi := 'chi_r in let chi2 := (chi :: chi^*)%CF in chi \in S -> [/\ {subset map nu chi2 <= 'Z[irr G]}, orthonormal (map nu chi2), chi - chi^*%CF \in 'Z[S, L^#] & (nu chi - nu chi^*)%CF 1%g == 0].
proof: Proof. move=> [[charS nrS ccS] [_ Ztau] oSS _ _] [[Inu Znu] Dnu] chi chi2 Schi. have sSZ: {subset S <= 'Z[S]} by apply: mem_zchar. have vcharS: {subset S <= 'Z[irr L]} by move=> phi /charS/char_vchar. have Schi2: {subset chi2 <= 'Z[S]} by apply/allP; rewrite /= !sSZ ?ccS. have Schi_diff: chi - chi^*%CF \in 'Z[S, L^#]. by rewrite sub_aut_zchar // zchar_onG sSZ ?ccS. split=> // [_ /mapP[xi /Schi2/Znu ? -> //]||]. apply: map_orthonormal; first by apply: sub_in2 Inu; apply: zchar_trans_on. rewrite orthonormalE (conjC_pair_orthogonal ccS) //=. by rewrite cfnorm_conjC !cfnorm_irr !eqxx. by rewrite -raddfB -cfunD1E Dnu // irr_vchar_on ?Ztau. 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)