no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f - g) ≫ h = f ≫ h - g ≫ h
rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, sub_def]