proposition: Lemma char_normal H G : H \char G -> H <| G.
proof: Proof. by move/char_normal_trans; apply; apply/andP; rewrite normG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)