F : Type ?u.218257
α : Type u_1
β : Type ?u.218263
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌈b⌉ ≤ ↑⌈a + b⌉ + 1 - a
F : Type ?u.218257
α : Type u_1
β : Type ?u.218263
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1
rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]
F : Type ?u.218257
α : Type u_1
β : Type ?u.218263
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ b + 1 ≤ ↑⌈a + b⌉ + 1 - a
F : Type ?u.218257
α : Type u_1
β : Type ?u.218263
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌈b⌉ ≤ ↑⌈a + b⌉ + 1 - a
refine' (ceil_lt_add_one _).le.trans _
F : Type ?u.218257
α : Type u_1
β : Type ?u.218263
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b ≤ ↑⌈a + b⌉
F : Type ?u.218257
α : Type u_1
β : Type ?u.218263
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ b + 1 ≤ ↑⌈a + b⌉ + 1 - a
rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]
no goals
F : Type ?u.218257
α : Type u_1
β : Type ?u.218263
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b ≤ ↑⌈a + b⌉
exact le_ceil _