proposition: Lemma cfdot_real_vchar_even phi psi : phi \in 'Z[irr G] /\ cfReal phi -> psi \in 'Z[irr G] /\ cfReal psi -> (2 %| '[phi, psi])%C = (2 %| '[phi, 1])%C || (2 %| '[psi, 1])%C.
proof: Proof. move=> [Zphi Rphi] [Zpsi Rpsi]; rewrite cfdot_vchar_r // (bigD1 (0 : 'I__)) //=. rewrite addrC -irr0 (bigID [pred i | conjC_Iirr i < i]%N) /=. set a1 := \sum_(i | _) _; set a2 := \sum_(i | _) _; suffices ->: a1 = a2. rewrite -mulr2n -[_ *+ 2]mulr_natr (rpredDl _ (dvdC_mull _ _)) //; last first. by rewrite rpred_sum // => i; rewrite rpredM ?Cint_cfdot_vchar_irr. have /CintP[m1 ->] := Cint_cfdot_vchar_irr 0 Zphi. have /CintP[m2 ->] := Cint_cfdot_vchar_irr 0 Zpsi. rewrite [m1]intEsign [m2]intEsign !rmorphMsign mulrACA -!mulrA !rpredMsign. by rewrite -natrM !(dvdC_nat 2) Euclid_dvdM. rewrite /a2 (reindex_inj (inv_inj (@conjC_IirrK _ _))) /=. apply: eq_big => [t | t _]; last first. by rewrite !conjC_IirrE !cfdot_real_conjC ?aut_Cint ?Cint_cfdot_vchar_irr. rewrite (inv_eq (@conjC_IirrK _ _)) conjC_IirrK -leqNgt ltn_neqAle val_eqE. rewrite -!(inj_eq irr_inj) !conjC_IirrE irr0 cfConjC_cfun1 odd_eq_conj_irr1 //. by rewrite andbA andbb. 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)