α : Type u_1
β : Type ?u.25
γ : Type ?u.28
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ b + 1
α : Type u_1
β : Type ?u.25
γ : Type ?u.28
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ ⌊↑(b + 1)⌋
rw [floor_intCast]
no goals
α : Type u_1
β : Type ?u.25
γ : Type ?u.28
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ b + 1
exact (lt_add_one _).le