simp only [tsub_le_iff_right]
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ - x ≤ 1
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ 1 + x