{A B C Y : AbGroup} (f : A $-> B) (g : A $-> C) (l : B $-> Y) (r : C $-> Y) (p : l o f == r o g) : ab_pushout_rec l r p $o ab_pushout_inr == r. Proof. intro x; simpl. rewrite (grp_homo_unit l). apply left_identity. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat.Core HSet. Require Import AbGroups.AbelianGroup AbGroups.Biproduct.