no goals
F : Type ?u.125097
α : Type u_1
β : Type ?u.125103
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ a < ↑⌊a⌋ + 1
simpa only [Int.succ, Int.cast_add, Int.cast_one] using lt_succ_floor a