proposition: Lemma subset_ortho_subcoherent S1 chi : {subset S1 <= S} -> chi \in S -> chi \notin S1 -> orthogonal S1 chi.
proof: Proof. move=> sS1S Schi S1'chi; apply/orthoPr=> phi S1phi; have Sphi := sS1S _ S1phi. have [_ _ /pairwise_orthogonalP[_ -> //]] := cohS. by apply: contraNneq S1'chi => <-. 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)