proposition: Lemma Dade_sub_lin_nonorthogonal nu1 nu2 zeta1 zeta2 : let S1 := seqIndD H1 L1 H1 1 in coherent_with S1 L1^# tau1 nu1 -> let S2 := seqIndD H2 L2 H2 1 in coherent_with S2 L2^# tau2 nu2 -> zeta1 \in irr L1 -> zeta1 \in S1 -> zeta1 1%g = #|L1 : H1|%:R -> zeta2 \in irr L2 -> zeta2 \in S2 -> zeta2 1%g = #|L2 : H2|%:R -> '[beta ddA1 zeta1, nu2 zeta2] != 0 \/ '[beta ddA2 zeta2, nu1 zeta1] != 0.
proof: Proof. move=> S1 cohS1 S2 cohS2 irr_zeta1 Szeta1 zeta1_1 irr_zeta2 Szeta2 zeta2_1. apply/nandP; pose Delta ddA nu zeta := beta ddA zeta + nu zeta. have Delta_context L H (A := H^#) ddA (tau := Dade ddA) nu zeta : let S := seqIndD H L H 1 in coherent_with S L^# tau nu -> zeta \in irr L -> zeta \in S -> zeta 1%g = #|L : H|%:R -> let D := Delta L H ddA nu zeta in '[D, 1] = 1 /\ D \in 'Z[irr G] /\ cfReal D. - move=> S cohS irr_zeta Szeta zeta_1 D. have [[nsHL oddL] [[_ Znu] nu_tau]] := (odd_Dade_context ddA, cohS). have ntS: (size S > 1)%N by apply: seqInd_nontrivial Szeta. have [[nuS1_0 beta1_1 Zbeta] _ _] := Dade_Ind1_sub_lin cohS ntS irr_zeta Szeta zeta_1. rewrite cfdotDl {}beta1_1 {nuS1_0}(orthoPr nuS1_0) ?map_f // addr0. rewrite rpredD ?{}Znu ?seqInd_zcharW {Zbeta}// /cfReal; do !split=> //. rewrite rmorphD /= -subr_eq0 opprD addrAC addrA -addrA addr_eq0 opprD. rewrite (cfConjC_Dade_coherent cohS) // opprK -Dade_conjC -!raddfB /=. rewrite nu_tau ?zcharD1_seqInd ?seqInd_sub_aut_zchar //=. by rewrite rmorphB /= conj_cfInd cfConjC_cfun1 opprB addrC addrA subrK. have: ~~ (2 %| '[Delta L1 H1 ddA1 nu1 zeta1, Delta L2 H2 ddA2 nu2 zeta2])%C. have /Delta_context/(_ irr_zeta1 Szeta1 zeta1_1)[Delta1_1 ZR_Delta1] := cohS1. have /Delta_context/(_ irr_zeta2 Szeta2 zeta2_1)[Delta2_1 ZR_Delta2] := cohS2. by rewrite cfdot_real_vchar_even // Delta1_1 Delta2_1 (dvdC_nat 2 1). rewrite cfdotDl !cfdotDr disjoint_Dade_ortho // add0r addrC cfdotC. apply: contra => /andP[/eqP-> /eqP->]; rewrite conjC0 add0r addr0. by rewrite (disjoint_coherent_ortho cohS1 cohS2) ?dvdC0. Qed.
imports: HB(structures) 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 commutator nilpotent frobenius) mathcomp(matrix mxalgebra mxrepresentation) odd_order(BGsection3) mathcomp(vector ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection4 PFsection5 PFsection6)