have : n ≤ m := Nat.le_of_succ_le_succ ‹step n ≤ step m›
n m : Nat
x✝ : n < m
this✝ : step n ≤ m
this : step n ≤ step m
⊢ lt n m
n m : Nat
x✝ : n < m
this✝¹ : step n ≤ m
this✝ : step n ≤ step m
this : n ≤ m
⊢ lt n m