proposition: Lemma pair_degree_coherence L G S (tau : {linear _ -> 'CF(gval G)}) R : subcoherent S tau R -> {in S &, forall phi1 phi2 : 'CF(gval L), phi1 1%g == phi2 1%g -> exists S1 : seq 'CF(L), [/\ phi1 \in S1, phi2 \in S1, cfConjC_subset S1 S & coherent S1 L^# tau]}.
proof: Proof. move=> scohS phi1 phi2 Sphi1 Sphi2 /= eq_phi12_1. have [[N_S _ ccS] _ _ _ _] := scohS. pose S1 := undup (phi1 :: phi1^* :: phi2 :: phi2^*)%CF. have sS1S: cfConjC_subset S1 S. split=> [|chi|chi]; rewrite ?undup_uniq //= !mem_undup; move: chi; apply/allP. by rewrite /= !ccS ?Sphi1 ?Sphi2. by rewrite /= !inE !cfConjCK !eqxx !orbT. exists S1; rewrite !mem_undup !inE !eqxx !orbT; split=> //. apply: uniform_degree_coherence (subset_subcoherent scohS sS1S) _. apply/(@all_pred1_constant _ (phi2 1%g))/allP=> _ /mapP[chi S1chi ->] /=. rewrite mem_undup in S1chi; move: chi S1chi; apply/allP. by rewrite /= !cfAut_char1 ?N_S // eqxx eq_phi12_1. 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)