simp only [Nat.one_le_ceil_iff, Real.sqrt_pos, Nat.cast_pos]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ⌈√↑N⌉₊
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 < N