case isFalse =>
  split at h
  case isTrue =>
    have : n = m := by assumption
    contradiction
  case isFalse =>
    have : ¬(n < m) := by assumption
    have : ¬(n = m) := by assumption
    have : n > m ∨ n ≤ m := Nat.lt_or_ge m n
    match ‹n > m ∨ n ≤ m› with
    | Or.inl (_ : n > m) =>
      have : m < n := ‹n > m›
      have : lt m n := prelude_lt_iff_impl_lt.mp ‹m < n›
      exact this
    | Or.inr (_ : n ≤ m) =>
      have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
      match ‹n = m ∨ n < m› with
      | Or.inl (_ : n = m) =>
        exact absurd ‹n = m› ‹¬(n = m)›
      | Or.inr (_ : n < m) =>
        exact absurd ‹n < m› ‹¬(n < m)›
n m : Nat
h✝ : ¬n < m
h : (if n = m then Ordering.eq else Ordering.gt) = Ordering.gt
⊢ lt m n
no goals