have : le n m := prelude_le_iff_impl_le.mp ‹n ≤ m›
n m : Nat
x✝ : n < m
this✝¹ : step n ≤ m
this✝ : step n ≤ step m
this : n ≤ m
⊢ lt n m
n m : Nat
x✝ : n < m
this✝² : step n ≤ m
this✝¹ : step n ≤ step m
this✝ : n ≤ m
this : le n m
⊢ lt n m