proposition: Lemma eq_homgl gT aT rT (G : {group gT}) (H : {group aT}) (K : {group rT}) : G \isog H -> homg G K = homg H K.
proof: Proof. by rewrite isogEhom => /andP[homGH homHG]; apply/idP/idP; apply: homg_trans. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)