proposition: Lemma ab_pushout_rec_beta_right {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: Proof. intro x; simpl. rewrite (grp_homo_unit l). apply left_identity. Defined.
imports: Basics Types Truncations.Core Modalities.ReflectiveSubuniverse WildCat.Core HSet Algebra.Groups.Image Algebra.Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.Biproduct