proposition: Lemma isog_trans : G \isog H -> H \isog K -> G \isog K.
proof: Proof. case/isogP=> f injf <-; case/isogP=> g injg <-. have defG: f @*^-1 (f @* G) = G by rewrite morphimGK ?subsetIl. rewrite -morphim_comp -{1 8}defG. by apply/isogP; exists [morphism of g \o f]; rewrite ?injm_comp. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)