F : Type ?u.92323
α : Type u_1
β : Type ?u.92329
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
⊢ a + b ≤ ↑⌈a⌉₊ + ↑⌈b⌉₊
F : Type ?u.92323
α : Type u_1
β : Type ?u.92329
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
⊢ ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
rw [ceil_le, Nat.cast_add]
no goals
F : Type ?u.92323
α : Type u_1
β : Type ?u.92329
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
⊢ a + b ≤ ↑⌈a⌉₊ + ↑⌈b⌉₊
exact _root_.add_le_add (le_ceil _) (le_ceil _)