proposition: Lemma char_norms H G : H \char G -> 'N(G) \subset 'N(H).
proof: Proof. case/charP=> sHG chHG; apply/normsP=> x /normP-Nx. have:= chHG [morphism of conjgm G x] => /=. by rewrite !morphimEsub //=; apply; rewrite // injm_conj. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)