proposition: Lemma normedTI_S A B G L : A != set0 -> L \subset 'N(A) -> A \subset B -> normedTI B G L -> normedTI A G L.
proof: Proof. move=> nzA /subsetP nAL /subsetP sAB /normedTI_memJ_P[nzB sLG tiB]. apply/normedTI_memJ_P; split=> // a x Aa Gx. by apply/idP/idP => [Aax | /nAL/memJ_norm-> //]; rewrite -(tiB a) ?sAB. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)