proposition: Lemma charY G H K : H \char G -> K \char G -> H <*> K \char G.
proof: Proof. case/charP=> sHG chHG; case/charP=> sKG chKG. apply/charP; split=> [|f injf Gf]; first by rewrite gen_subG subUset sHG. by rewrite morphim_gen ?(morphimU, subUset, sHG, chHG, chKG). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)