have : ∃ k, n + k ≃ step m' := Exists.intro (step k) ‹n + step k ≃ step m'›
n m m' : Nat
a✝ : n ≤ m'
this✝ : le n m'
k : Nat
h✝ : n + k ≃ m'
this : n + step k ≃ step m'
⊢ le n (step m')
n m m' : Nat
a✝ : n ≤ m'
this✝¹ : le n m'
k : Nat
h✝ : n + k ≃ m'
this✝ : n + step k ≃ step m'
this : ∃ k, n + k ≃ step m'
⊢ le n (step m')