∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K X Y : C} (i : K ⟶ X) {f : X ⟶ Y},
  CategoryTheory.CategoryStruct.comp i f = 0 → CategoryTheory.CategoryStruct.comp f.op i.op = 0