rfl
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = ⌈x⌉₊.succ - 1

case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊