no goals
F : Type ?u.57635
α : Type u_1
β : Type ?u.57641
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n
rw [← ceil_le, ← not_le, ← ceil_le, not_le,
  tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
  le_antisymm_iff, and_comm]