proposition: Lemma constt_charP (i : Iirr G) chi : chi \is a character -> reflect (exists2 chi', chi' \is a character & chi = 'chi_i + chi') (i \in irr_constt chi).
proof: Proof. move=> Nchi; apply: (iffP idP) => [i_in_chi| [chi' Nchi' ->]]; last first. rewrite inE /= cfdotDl cfdot_irr eqxx -(eqP (Cnat_cfdot_char_irr i Nchi')). by rewrite -natrD pnatr_eq0. exists (chi - 'chi_i); last by rewrite addrC subrK. apply/forallP=> j; rewrite coord_cfdot cfdotBl cfdot_irr. have [<- | _] := eqP; last by rewrite subr0 Cnat_cfdot_char_irr. move: i_in_chi; rewrite inE; case/natrP: (Cnat_cfdot_char_irr i Nchi) => n ->. by rewrite pnatr_eq0 -lt0n => /natrB <-; apply: rpred_nat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)