proposition: Lemma isogEcard rT aT (G : {group rT}) (H : {group aT}) : (G \isog H) = (homg G H) && (#|H| <= #|G|).
proof: Proof. rewrite isog_sym; apply/isogP/andP=> [[f injf <-] | []]. by rewrite leq_eqVlt eq_sym card_im_injm injf morphim_homg. case/homgP=> f <-; rewrite leq_eqVlt eq_sym card_im_injm. by rewrite ltnNge leq_morphim orbF; exists f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)