by_cases x = y using Complemented with
| .isTrue rfl => left; right; rfl
| .isFalse hne =>
  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 : α
⊢ reflRel r x y ∨ reflRel r y x
no goals