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