proposition: Lemma subcoherent_norm chi psi (tau1 : {additive 'CF(L) -> 'CF(G)}) X Y : [/\ chi \in S, psi \in 'Z[irr L] & orthogonal (chi :: chi^*)%CF psi] -> let S0 := chi - psi :: chi - chi^*%CF in {in 'Z[S0], isometry tau1, to 'Z[irr G]} -> tau1 (chi - chi^*%CF) = tau (chi - chi^*%CF) -> [/\ tau1 (chi - psi) = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)] -> [/\ '[chi] <= '[X] & '[psi] <= '[Y] -> [/\ '[X] = '[chi], '[Y] = '[psi] & exists2 E, subseq E (R chi) & X = \sum_(xi <- E) xi]].
proof: Proof. case=> Schi Zpsi /and3P[/andP[/eqP-ochi_psi _] /andP[/eqP-ochic_psi _] _] S0. move=> [Itau1 Ztau1] tau1dchi [defXY oXY oYR]. have [[ZS nrS ccS] [tS Zt] oS /(_ _ Schi)[ZR o1R tau_dchi] _] := cohS. have [/=/andP[S'0 uS] oSS] := pairwise_orthogonalP oS. have [nRchi Schic] := (hasPn nrS _ Schi, ccS _ Schi). have ZtauS00: tau1 S0`_0 \in 'Z[irr G] by rewrite Ztau1 ?mem_zchar ?mem_head. have{ZtauS00} [X1 R_X1 [Y1 [dXY1 oXY1 oY1R]]] := subcoherent_split Schi ZtauS00. have [uR _] := orthonormalP o1R; have [a Za defX1] := zchar_expansion uR R_X1. have dotS00R xi: xi \in R chi -> '[tau1 S0`_0, xi] = a xi. move=> Rxi; rewrite dXY1 cfdotBl (orthoPl oY1R) // subr0. by rewrite defX1 cfproj_sum_orthonormal. have nchi: '[chi] = \sum_(xi <- R chi) a xi. transitivity '[tau1 S0`_0, tau1 S0`_1]; last first. by rewrite tau1dchi tau_dchi cfdot_sumr; apply: eq_big_seq dotS00R. rewrite [RHS]cfdotC Itau1 ?mem_zchar ?mem_nth // cfdotBl !cfdotBr. by rewrite ochi_psi ochic_psi (oSS chi^*%CF) // !subr0 -cfdotC. have normX: '[X1] <= '[X] ?= iff (X == X1). rewrite -[in '[X]](subrK X1 X) -subr_eq0 cfnormDd. by rewrite -leifBLR subrr -cfnorm_eq0 eq_sym; apply/leif_eq/cfnorm_ge0. rewrite defX1 cfdot_sumr big1_seq // => xi Rxi. rewrite cfdotZr cfdotBl cfproj_sum_orthonormal // -{2}dotS00R // defXY. by rewrite cfdotBl (orthoPl oYR) // subr0 subrr mulr0. pose is01a xi := a xi == (a xi != 0)%:R. have leXa xi: a xi <= `|a xi| ^+ 2 ?= iff is01a xi. rewrite Cint_normK //; split; first by rewrite Cint_ler_sqr. rewrite eq_sym -subr_eq0 -[lhs in _ - lhs]mulr1 -mulrBr mulf_eq0 subr_eq0. by rewrite /is01a; case a_xi_0: (a xi == 0). have{nchi normX} part_a: '[chi] <= '[X] ?= iff all is01a (R chi) && (X == X1). apply: leif_trans normX; rewrite nchi defX1 cfnorm_sum_orthonormal //. by rewrite -big_all !(big_tnth _ _ (R chi)) big_andE; apply: leif_sum. split=> [|/leif_eq part_b]; first by case: part_a. have [_ /esym] := leifD part_a part_b; rewrite -!cfnormBd // -defXY. rewrite Itau1 ?mem_zchar ?mem_head // eqxx => /andP[a_eq /eqP->]. split=> //; first by apply/esym/eqP; rewrite part_a. have{a_eq} [/allP a01 /eqP->] := andP a_eq; rewrite defX1. exists [seq xi <- R chi | a xi != 0]; first exact: filter_subseq. rewrite big_filter [rhs in _ = rhs]big_mkcond /=. by apply: eq_big_seq => xi Rxi; rewrite -mulrb -scaler_nat -(eqP (a01 _ _)). 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)