by_cases a_zero : a = 0
case h
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
⊢ b ≤ ↑a
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : a = 0
⊢ b ≤ ↑a

case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
⊢ b ≤ ↑a