proposition: Lemma sum_seqIndD_square : H <| L -> M <| L -> M \subset H -> \sum_(phi <- S) phi 1%g ^+ 2 / '[phi] = #|L : H|%:R * (#|H : M|%:R - 1).
proof: Proof. move=> nsHL nsML sMH; rewrite -(Lagrange_index sKL sHK) natrM -/e -mulrA. rewrite -sum_Iirr_kerD_square ?(normalS _ sKL) ?(subset_trans sMH) //. pose h i := @Ordinal (size S).+1 _ (index_size ('Ind 'chi[K]_i) S). rewrite (partition_big h (ltn^~ (size S))) => /= [|i Xi]; last first. by rewrite index_mem mem_seqInd. rewrite big_distrr big_ord_narrow //= big_index_uniq ?seqInd_uniq //=. apply: eq_big_seq => phi Sphi; rewrite /eq_op insubT ?index_mem //= => _. have /seqIndP[i kHMi def_phi] := Sphi. have/cfunP/(_ 1%g) := scaled_cfResInd_sum_cfclass i nsKL. rewrite !cfunE sum_cfunE -def_phi cfResE // mulrAC => ->; congr (_ * _). rewrite reindex_cfclass //=; apply/esym/eq_big => j; last by rewrite !cfunE. rewrite (sameP (cfclass_Ind_irrP _ _ nsKL) eqP) -def_phi -mem_seqInd //. by apply/andP/eqP=> [[Sj /eqP/(congr1 (nth 0 S))] | ->]; rewrite ?nth_index. 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)