cases Connex.connex (r:=r) hne with
| inl hxy => left; left; exact hxy
| inr hyx => right; left; exact hyx
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
⊢ reflRel r x y ∨ reflRel r y x
no goals