simp only [add_sub_cancel, and_true]
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌊x⌋₊ - x| ≤ 1 ∧ ↑⌊x⌋₊ = x + (↑⌊x⌋₊ - x)
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌊x⌋₊ - x| ≤ 1