F : Type ?u.217435
α : Type u_1
β : Type ?u.217441
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b ≤ ↑⌈a⌉ + ↑⌈b⌉
F : Type ?u.217435
α : Type u_1
β : Type ?u.217441
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉
rw [ceil_le, Int.cast_add]
no goals
F : Type ?u.217435
α : Type u_1
β : Type ?u.217441
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b ≤ ↑⌈a⌉ + ↑⌈b⌉
exact add_le_add (le_ceil _) (le_ceil _)