proposition: Lemma morphpre_norm R : f @*^-1 'N(R) \subset 'N(f @*^-1 R).
proof: Proof. by apply/subsetP=> x /[!inE] /andP[Dx Nfx]; rewrite -morphpreJ ?morphpreS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)