proposition: Lemma char_normal_trans H G K : K \char H -> H <| G -> K <| G.
proof: Proof. move=> chKH /andP[sHG nHG]. by rewrite /normal (subset_trans (char_sub chKH)) // (char_norm_trans chKH). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)