have : n ≤ m' := prelude_le_from_impl_le ‹le n m'›
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝² : step (n + k') ≃ step m'
this✝¹ : n + k' ≃ m'
this✝ : ∃ k', n + k' ≃ m'
this : le n m'
⊢ n ≤ step m'
n m' k' : Nat
h✝ : n + step k' ≃ step m'
this✝³ : step (n + k') ≃ step m'
this✝² : n + k' ≃ m'
this✝¹ : ∃ k', n + k' ≃ m'
this✝ : le n m'
this : n ≤ m'
⊢ n ≤ step m'