{A B : AbGroup} {f g : A $-> B} {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g) : ab_coeq_rec i p $o ab_coeq_in $== i := fun _ => idpath.
Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import Groups.QuotientGroup AbelianGroup Biproduct.