next hne =>
  split
  next => rfl
  next =>
    split
    next =>
      absurd hne
      symmetry
      assumption
    next =>
      cases Connex.connex (r:=(.<.)) hne with
      | inl _ => contradiction
      | inr _ => contradiction
case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
⊢ gt.swap = if y < x then lt else if y = x then eq else gt
no goals