∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {A B C : V} (f : A ⟶ B) (g : B ⟶ C) {Z : V} (h : Z ⟶ A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f) g = 0 →
    CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp f g) =
      CategoryTheory.CategoryStruct.comp h 0