F : Type ?u.46418
α : Type u_1
β : Type ?u.46424
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
⊢ a ≤ ↑⌊a⌋₊ + 1
F : Type ?u.46418
α : Type u_1
β : Type ?u.46424
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
⊢ ⌈a⌉₊ ≤ ⌊a⌋₊ + 1
rw [ceil_le, Nat.cast_add, Nat.cast_one]
no goals
F : Type ?u.46418
α : Type u_1
β : Type ?u.46424
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
⊢ a ≤ ↑⌊a⌋₊ + 1
exact (lt_floor_add_one a).le