{G : Group} {A : AbGroup} (f : G $-> A) `{IsEmbedding f} : AbGroup := QuotientAbGroup _ (grp_image_embedding f).
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.