obtain ⟨C₂, hC₂_le, hC₂⟩ := nat_div_approx (Nat.ceil x - 1) d
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
case intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5