Rounding errors in the number of integers in a short interval

theorem NairTenenbaum.shortInterval_card_bounds {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : y - 1 ≤ ↑(shortInterval x y).card ∧ ↑(shortInterval x y).card ≤ y + 1

theorem NairTenenbaum.shortInterval_card_le_twice {x y : ℝ} (hx : 0 ≤ x) (hy : 1 ≤ y) : ↑(shortInterval x y).card ≤ 2 * y