∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] (X Y Z : C)
  (f : X ⟶ Y) (g h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (g + h) =
    CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h