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