proposition: Corollary coherent_ortho S1 S2 (tau1 tau2 : {additive 'CF(L) -> 'CF(G)}) : cfConjC_subset S1 S -> coherent_with S1 L^# tau tau1 -> cfConjC_subset S2 S -> coherent_with S2 L^# tau tau2 -> {subset S2 <= [predC S1]} -> orthogonal (map tau1 S1) (map tau2 S2).
proof: Proof. move=> uccS1 cohS1 uccS2 cohS2 S1'2; have [_ sS2S _] := uccS2. apply/orthogonalP=> mu _ S1mu /mapP[phi S2phi ->]. have [e /mem_subseq Re ->] := mem_coherent_sum_subseq uccS2 cohS2 S2phi. rewrite cfdot_sumr big1_seq // => xi {e}/Re; apply: orthogonalP mu xi S1mu. by apply: coherent_ortho_supp; rewrite ?sS2S //; apply: S1'2. 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)