no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
rw [add_def, comp_sub, neg_def, comp_sub, comp_zero, add_def, neg_def]