F : Type ?u.210054
α : Type u_1
β : Type ?u.210060
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ a ≤ ↑⌊a⌋ + 1
F : Type ?u.210054
α : Type u_1
β : Type ?u.210060
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ ⌈a⌉ ≤ ⌊a⌋ + 1
rw [ceil_le, Int.cast_add, Int.cast_one]
no goals
F : Type ?u.210054
α : Type u_1
β : Type ?u.210060
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ a ≤ ↑⌊a⌋ + 1
exact (lt_floor_add_one a).le