proposition: Lemma isoGrp_trans gT rT (G : {group gT}) (H : {group rT}) p : G \isog H -> H \isog Grp p -> G \isog Grp p.
proof: Proof. by move=> isoGH isoHp kT K; rewrite -isoHp; apply: eq_homgr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq) mathcomp(fintype finset fingroup morphism)