F : Type ?u.132012
α : Type u_1
β : Type ?u.132018
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ ↑⌊b⌋
F : Type ?u.132012
α : Type u_1
β : Type ?u.132018
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋
rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]
F : Type ?u.132012
α : Type u_1
β : Type ?u.132018
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ b - 1
F : Type ?u.132012
α : Type u_1
β : Type ?u.132018
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ ↑⌊b⌋
refine' le_trans _ (sub_one_lt_floor _).le
F : Type ?u.132012
α : Type u_1
β : Type ?u.132018
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ ≤ a + b
F : Type ?u.132012
α : Type u_1
β : Type ?u.132018
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ b - 1
rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]
no goals
F : Type ?u.132012
α : Type u_1
β : Type ?u.132018
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ ≤ a + b
exact floor_le _