no goals
F : Type ?u.129440
α : Type u_1
β : Type ?u.129446
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝¹ a✝ : α
z a : ℤ
⊢ a ≤ ⌊a✝ + ↑z⌋ ↔ a ≤ ⌊a✝⌋ + z
rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]