proposition: Theorem prTIind_irr_cases ell (phi := 'chi_ell) : {i : _ & {j | phi = mu2_ i j}} + {k | k \notin codom Ichi & phi = 'Ind 'chi_k}.
proof: Proof. have [k] := constt_cfRes_irr K ell; rewrite -constt_Ind_Res => kLell. have [[j Dk] | [/irrP/sig_eqW[l1 DkL] chi'k]] := prTIres_irr_cases k. have [i /=/eqP <- | mu2j'l] := pickP (fun i => mu2_ i j == phi). by left; exists i, j. case/eqP: kLell; rewrite Dk cfInd_prTIres cfdot_suml big1 // => i _. by rewrite cfdot_irr -(inj_eq irr_inj) mu2j'l. right; exists k; last by move: kLell; rewrite DkL constt_irr inE => /eqP <-. apply/codomP=> [[j Dk]]; have/negP[] := prTIred_not_irr j. by rewrite -cfInd_prTIres -Dk DkL mem_irr. 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)