proposition: Lemma rem_irr1 (xi phi : 'CF('SG_n)) : xi \in irr 'SG_n -> phi \is a character -> '[phi, xi] != 0 -> phi - xi \is a character.
proof: Proof. move=> /irrP[i ->{xi}] Hphi. rewrite -irr_consttE => /(constt_charP i Hphi) [psi Hpsi ->{phi Hphi}]. by rewrite [_ + psi]addrC addrK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama