have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this : n ≤ m
⊢ n < m
n m : Nat
x✝ : lt n m
left✝ : le n m
right✝ : n ≄ m
this✝ : n ≤ m
this : n = m ∨ n < m
⊢ n < m