a✝ b✝ : ℤ
n : ℕ
a b : ℤ
h : a ≤ b
⊢ a ≤ ↑(toNat b)
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
h : a ≤ b
⊢ toNat a ≤ toNat b
rw [toNat_le]
no goals
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
h : a ≤ b
⊢ a ≤ ↑(toNat b)
exact le_trans h (self_le_toNat b)