proposition: Lemma dual_coherence S tau R nu : subcoherent S tau R -> coherent_with S L^# tau nu -> (size S <= 2)%N -> coherent_with S L^# tau (dual_iso nu).
proof: Proof. move=> [[charS nrS ccS] _ oSS _ _] [[Inu Znu] Dnu] szS2. split=> [|{Inu Znu oSS} phi ZSphi]. have{oSS} ccZS := cfAut_zchar ccS. have vcharS: {subset S <= 'Z[irr L]} by move=> phi /charS/char_vchar. split=> [phi1 phi2 Sphi1 Sphi2 | phi Sphi]. rewrite cfdotNl cfdotNr opprK Inu ?ccZS // cfdot_conjC aut_Cint //. by rewrite Cint_cfdot_vchar ?(zchar_sub_irr vcharS). by rewrite rpredN Znu ?ccZS. rewrite -{}Dnu //; move: ZSphi; rewrite zcharD1E => /andP[]. case/zchar_nth_expansion=> x Zx -> {phi} /=. case: S charS nrS ccS szS2 x Zx => [_ _ _ _ x _| eta S1]. by rewrite big_ord0 !raddf0. case/allP/andP=> Neta _ /norP[eta'c _] /allP/andP[S1_etac _]. rewrite inE [_ == _](negPf eta'c) /= in S1_etac. case S1E: S1 S1_etac => [|u []] // /predU1P[] //= <- _ z Zz. rewrite big_ord_recl big_ord1 !raddfD/= !raddfZ_Cint //=. rewrite !cfunE/= (conj_Cnat (Cnat_char1 Neta)) -mulrDl mulf_eq0. rewrite addr_eq0 char1_eq0 // !scalerN /= cfConjCK addrC. by case/pred2P => ->; rewrite ?raddf0 //= !scaleNr opprK. 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)