proposition: Lemma morphim_subnormG A G : 'ker f \subset G -> G \subset D -> f @* 'N_A(G) = 'N_(f @* A)(f @* G).
proof: Proof. move=> sKB sBD; rewrite morphimIG ?normsG // morphim_normG //. by rewrite setICA setIA morphimIim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)