rw[←add_le_add_iff_right 1]
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1) ≤ x + y

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1) + 1 ≤ x + y + 1

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y