proposition: Lemma size_irr_subseq_seqInd S1 : subseq S1 S -> {subset S1 <= irr L} -> (#|L : K| * size S1 = #|[set i | 'Ind 'chi[K]_i \in S1]|)%N.
proof: Proof. move=> sS1S irrS1; have uniqS1: uniq S1 := subseq_uniq sS1S seqInd_uniq. rewrite (card_imset_Ind_irr nsKL) => [|i|i y]; first 1 last. - by rewrite inE => /irrS1. - by rewrite !inE => *; rewrite conjg_IirrE -(cfConjgInd _ _ nsKL) ?cfConjg_id. congr (_ * _)%N; transitivity #|map cfIirr S1|. rewrite (card_uniqP _) ?size_map ?map_inj_in_uniq //. exact: sub_in2 irrS1 _ (can_in_inj (@cfIirrE _ _)). apply: eq_card => s; apply/idP/imsetP=> [/mapP[phi S1phi] | [i S1iG]] {s}->. have /seqIndP[i _ Dphi]: phi \in S := mem_subseq sS1S S1phi. by exists i; rewrite ?inE -Dphi. by apply: map_f; rewrite inE in S1iG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)