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