α : Type u_1
β : Type ?u.2623
γ : Type ?u.2626
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b - 1 ≤ b
α : Type u_1
β : Type ?u.2623
γ : Type ?u.2626
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ ⌈↑(b - 1)⌉ ≤ b
rw [ceil_intCast]
no goals
α : Type u_1
β : Type ?u.2623
γ : Type ?u.2626
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b - 1 ≤ b
exact (sub_one_lt _).le