proposition: Lemma isog_hom rT aT (G : {group rT}) (H : {group aT}) : G \isog H -> homg G H.
proof: Proof. by rewrite isogEcard; case/andP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)