proposition: Theorem prTIres_spec j : chi_ j = 'Res (mu2_ 0 j) /\ mu_ j = 'Ind (chi_ j).
proof: Proof. rewrite /Ichi; set chi_j := 'Res _. have [k chi_j_k]: {k | k \in irr_constt chi_j} := constt_cfRes_irr K _. have Nchi_j: chi_j \is a character by rewrite cfRes_char ?irr_char. have lb_mu_1: w1%:R * 'chi_k 1%g <= mu_ j 1%g ?= iff (chi_j == 'chi_k). have [chi' Nchi' Dchi_j] := constt_charP _ Nchi_j chi_j_k. rewrite prTIred_1 (mono_leif (ler_pM2l (gt0CG W1))). rewrite -subr_eq0 Dchi_j addrC addKr -(canLR (addrK _) Dchi_j) !cfunE. rewrite leifBLR addrC -leifBLR cfRes1 subrr -char1_eq0 // eq_sym. by apply: leif_eq; rewrite char1_ge0. pose psi := 'Ind 'chi_k - mu_ j; have Npsi: psi \is a character. apply/forallP=> l; rewrite coord_cfdot cfdotBl; set a := '['Ind _, _]. have Na: a \in Cnat by rewrite Cnat_cfdot_char_irr ?cfInd_char ?irr_char. have [[i /eqP Dl] | ] := altP (@existsP _ (fun i => 'chi_l == mu2_ i j)). have [n Da] := CnatP a Na; rewrite Da cfdotC Dl cfdot_prTIirr_red. rewrite rmorph_nat -natrB ?Cnat_nat // eqxx lt0n -eqC_nat -Da. by rewrite -irr_consttE constt_Ind_Res Dl cfRes_prTIirr_eq0. rewrite negb_exists => /forallP muj'l. rewrite cfdot_suml big1 ?subr0 // => i _. rewrite cfdot_irr -(inj_eq irr_inj) mulrb ifN_eqC ?muj'l //. have ub_mu_1: mu_ j 1%g <= 'Ind[L] 'chi_k 1%g ?= iff ('Ind 'chi_k == mu_ j). rewrite -subr_eq0 -/psi (canRL (subrK _) (erefl psi)) cfunE -leifBLR. by rewrite subrr -char1_eq0 // eq_sym; apply: leif_eq; rewrite char1_ge0. have [_ /esym] := leif_trans lb_mu_1 ub_mu_1; rewrite cfInd1 //. by rewrite -(index_sdprod defL) eqxx => /andP[/eqP-> /eqP <-]; rewrite irrK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)