intro hne
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
⊢ x ≠ y → coRel r x y ∨ coRel r y x
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ coRel r x y ∨ coRel r y x