no goals
F : Type ?u.45610
α : Type u_1
β : Type ?u.45616
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ 1 ≤ ⌈a⌉₊ ↔ 0 < a
rw [← zero_add 1, Nat.add_one_le_ceil_iff, Nat.cast_zero]