proposition: Lemma morphim_normG G : 'ker f \subset G -> G \subset D -> f @* 'N(G) = 'N_(f @* D)(f @* G).
proof: Proof. move=> sKG sGD; apply/eqP; rewrite eqEsubset -{1}morphimIdom morphim_subnorm. rewrite -(morphpreK (subsetIl _ _)) morphimS //= morphpreI subIset // orbC. by rewrite -{2}(morphimGK sKG sGD) morphpre_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)