proposition: Lemma subcoherent_split chi beta : chi \in S -> beta \in 'Z[irr G] -> exists2 X, X \in 'Z[R chi] & exists Y, [/\ beta = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)].
proof: Proof. move=> Schi Zbeta; have [_ _ _ /(_ _ Schi)[ZR oRR _] _] := cohS. have [X RX [Y [defXY oXY oYR]]] := orthogonal_split (R chi) beta. exists X; last first. by exists (- Y); rewrite opprK (orthogonal_oppl Y) cfdotNr oXY oppr0. have [_ -> ->] := orthonormal_span oRR RX; rewrite big_seq rpred_sum // => a Ra. rewrite rpredZ_Cint ?mem_zchar // -(addrK Y X) -defXY. by rewrite cfdotBl (orthoPl oYR) // subr0 Cint_cfdot_vchar // ZR. 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)