proposition: Lemma isogEhom rT aT (G : {group rT}) (H : {group aT}) : (G \isog H) = homg G H && homg H G.
proof: Proof. apply/idP/andP=> [isoGH | [homGH homHG]]. by rewrite !isog_hom // isog_sym. by rewrite isogEcard homGH leq_homg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)