no goals
F : Type ?u.139599
α : Type u_1
β : Type ?u.139605
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
  and_comm]