proposition: Lemma subset_subcoherent S1 : cfConjC_subset S1 S -> subcoherent S1 tau R.
proof: Proof. case=> uS1 sS1 ccS1; have [[N_S nrS _] Itau oS defR oR] := cohS. split; last 1 [exact: sub_in1 defR | exact: sub_in2 oR]. - split=> // [xi /sS1/N_S// | ]. by apply/hasPn; apply: sub_in1 (hasPn nrS). - by apply: sub_iso_to Itau => //; apply: zchar_subset. exact: sub_pairwise_orthogonal oS. 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)