no goals
F : Type ?u.207706
α : Type u_1
β : Type ?u.207712
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a : α
z : ℤ
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z
rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]