proposition: Lemma cfConjC_Dade_coherent K H M (calS := seqIndD K L H M) tau1 chi : coherent_with calS L^# (Dade ddA) tau1 -> [/\ odd #|G|, K <| L & H \subset K] -> chi \in irr L -> chi \in calS -> (tau1 chi)^*%CF = tau1 chi^*%CF.
proof: Proof. move=> cohS [oddG nsKL sHK] irr_chi Schi. apply: (cfAut_Dade_coherent cohS) => //; split; last exact: cfAut_seqInd. have oddL: odd #|L| by apply: oddSg oddG; have [_] := ddA. exact: seqInd_nontrivial_irr Schi. 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)