proposition: Lemma charM G H K : H \char G -> K \char G -> H * K \char G.
proof: Proof. move=> chHG chKG; rewrite -norm_joinEl ?charY //. exact: subset_trans (char_sub chHG) (char_norm chKG). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)