proposition: Lemma typeP_reducible_core_Ind (ptiWM := FT_primeTI_hyp MtypeP) : [/\ size mu_ = p.-1, has predT mu_, {subset mu_ <= [seq primeTIred ptiWM j | j in predC1 0]} & {in mu_, forall mu_j, isIndHC mu_j}].
proof: Proof. have [[sz_mu _] /mulG_sub[sHHU _]] := (nb_redM_H0, sdprodW defHU). rewrite has_predT sz_mu -subn1 subn_gt0 prime_gt1 //; split=> // [mu_j|]. rewrite mem_filter => /andP[red_chi /seqIndP[s /setDP[_ kerH's] Dchi]]. have [[j Ds] | [/idPn[]]] := prTIres_irr_cases ptiWM s; last by rewrite -Dchi. rewrite Dchi Ds cfInd_prTIres image_f ?inE //=. by apply: contraNneq kerH's => j0; rewrite inE Ds j0 prTIres0 cfker_cfun1. have[/typeP_Galois_characters[_ _ []] // | Gal'M] := boolP typeP_Galois. by have [_ []] := typeP_nonGalois_characters Gal'M. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator center gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection8)