proposition: Lemma size_red_subseq_seqInd_typeP (calX : {set Iirr K}) calS1 : uniq calS1 -> {subset calS1 <= seqInd M calX} -> {subset calS1 <= [predC irr M]} -> size calS1 = #|[set i : Iirr K | 'Ind 'chi_i \in calS1]|.
proof: Proof. move=> uS1 sS1S redS1; pose h s := 'Ind[M, K] 'chi_s. apply/eqP; rewrite cardE -(size_map h) -uniq_size_uniq // => [|xi]; last first. apply/imageP/idP=> [[i] | S1xi]; first by rewrite inE => ? ->. by have /seqIndP[s _ Dxi] := sS1S _ S1xi; exists s; rewrite ?inE -?Dxi. apply/dinjectiveP; pose h1 xi := cfIirr (#|W1|%:R^-1 *: 'Res[K, M] xi). apply: can_in_inj (h1) _ => s; rewrite inE => /redS1 red_s. have cycW1: cyclic W1 by have [[]] := MtypeP. have [[j /irr_inj->] | [/idPn[]//]] := prTIres_irr_cases ptiWM s. by rewrite /h cfInd_prTIres /h1 cfRes_prTIred scalerK ?neq0CG ?irrK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)