exact absurd ‹n = m› ‹¬(n = m)›
n m : Nat
h✝³ : ¬n < m
h✝² : ¬n = m
h : Ordering.gt = Ordering.gt
this✝² : ¬n < m
this✝¹ : ¬n = m
this✝ : n > m ∨ n ≤ m
h✝¹ : n ≤ m
this : n = m ∨ n < m
h✝ : n = m
⊢ lt m n
no goals