left
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y ∨ coRel r y x
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y