constructor
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ coRel r x y ↔ r x y ∧ x ≠ y
case mp
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ coRel r x y → r x y ∧ x ≠ y

case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ r x y ∧ x ≠ y → coRel r x y