have : ¬(n = m) := by assumption
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this : ¬n < m
⊢ lt m n
n m : Nat
h✝¹ : ¬n < m
h✝ : ¬n = m
h : Ordering.gt = Ordering.gt
this✝ : ¬n < m
this : ¬n = m
⊢ lt m n