{G: Group} {A B : AbGroup} (f : G $-> A) `{IsEmbedding f} (h : A $-> B) (p : grp_homo_compose h f $== grp_homo_const) : ab_cokernel_embedding f $-> B. Proof. snrapply (grp_quotient_rec _ _ h). intros a [g q]. induction q. exact (p g). Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.