have hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ( ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) : ℝ) := by
  rw [Nat.cast_sub]
  gcongr
  rw[Nat.le_floor_iff]
  rw[←add_le_add_iff_right 1]
  norm_cast
  rw [Nat.sub_add_cancel (by simp [hx])]
  linarith [Nat.ceil_le_self_add_one x (le_of_lt hx)]
  linarith
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
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)
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5