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