proposition: Lemma char_norm_trans H G A : H \char G -> A \subset 'N(G) -> A \subset 'N(H).
proof: Proof. by move/char_norms=> nHnG nGA; apply: subset_trans nHnG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)