apply ind_on (motive := λ k => m ≤ k → n ≤ k) k
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ k → n ≤ k
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ 0 → n ≤ 0

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1