proposition: Lemma morphpre_subnorm R S : f @*^-1 'N_R(S) \subset 'N_(f @*^-1 R)(f @*^-1 S).
proof: Proof. by rewrite morphpreI setIS ?morphpre_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)