proposition: Lemma char_trans H G K : K \char H -> H \char G -> K \char G.
proof: Proof. case/charP=> sKH chKH; case/charP=> sHG chHG. apply/charP; split=> [|f injf Gf]; first exact: subset_trans sHG. rewrite -{1}(setIidPr sKH) -(morphim_restrm sHG) chKH //. by rewrite ker_restrm; move/trivgP: injf => ->; apply: subsetIr. by rewrite morphim_restrm setIid chHG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)