proposition: Lemma charI G H K : H \char G -> K \char G -> H :&: K \char G.
proof: Proof. case/charP=> sHG chHG; case/charP=> _ chKG. apply/charP; split=> [|f injf Gf]; first by rewrite subIset // sHG. by rewrite morphimGI ?(chHG, chKG) //; apply: subset_trans (sub1G H). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)