α : Type u_1
β : Type ?u.10951
γ : Type ?u.10954
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌊x⌋ ≤ x
α : Type u_1
β : Type ?u.10951
γ : Type ?u.10954
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌊x⌋ + 1) - 1 ≤ x
rw [cast_add, cast_one, add_sub_cancel]
no goals
α : Type u_1
β : Type ?u.10951
γ : Type ?u.10954
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌊x⌋ ≤ x
exact floor_le _