proposition: Lemma morphim_norm A : f @* 'N(A) \subset 'N(f @* A).
proof: Proof. apply/subsetP=> fx; case/morphimP=> x Dx Nx -> {fx}. by rewrite inE -morphimJ ?(normP Nx). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)