by_cases r x y using Complemented with
| .isTrue hxy => left; exact Asymmetric.asymm hxy
| .isFalse nxy => right; exact nxy
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y ∨ coRel r y x
no goals