proposition: Lemma Iirr_kerDS A1 A2 B1 B2 : A2 \subset A1 -> B1 \subset B2 -> Iirr_kerD B1 A1 \subset Iirr_kerD B2 A2.
proof: Proof. by move=> sA12 sB21; rewrite setDSS ?Iirr_kerS. 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)