proposition: Lemma morphim_subnorm A B : f @* 'N_A(B) \subset 'N_(f @* A)(f @* B).
proof: Proof. exact: subset_trans (morphimI A _) (setIS _ (morphim_norm B)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)