intro ⟨hxy, hne⟩ hyx
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ r x y ∧ x ≠ y → coRel r x y
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ False