by_cases r x y using Complemented with
| .isTrue hxy => left; exact hxy
| .isFalse cyx =>
  right
  by_contradiction
  | assuming hne =>
    cases Connex.connex (r:=r) hne with
    | inl hxy => absurd cyx; exact hxy
    | inr hyx => absurd cxy; exact hyx
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
⊢ reflRel r x y
no goals