`{Funext} {A B : AbGroup} (f : A $-> B) : GroupIsomorphism (QuotientAbGroup A (grp_kernel f)) (abgroup_image f). Proof. etransitivity. 2: rapply grp_first_iso. apply grp_iso_quotient_normal. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.