F : Type ?u.216510
α : Type u_1
β : Type ?u.216516
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ ⌈a⌉ < ⌈a⌉ + 1
F : Type ?u.216510
α : Type u_1
β : Type ?u.216516
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ ↑⌈a⌉ < a + 1
rw [← lt_ceil, ← Int.cast_one, ceil_add_int]
no goals
F : Type ?u.216510
α : Type u_1
β : Type ?u.216516
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ ⌈a⌉ < ⌈a⌉ + 1
apply lt_add_one