rw [←Logic.nand_iff_not_or_not]
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ ¬(r z x ∧ r y z)