by_contradiction
| assuming hne =>
  cases Connex.connex (r:=r) hne with
  | inl hxy => absurd cyx; exact hxy
  | inr hyx => absurd cxy; exact hyx
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
⊢ x = y
no goals