F : Type ?u.151819
α : Type u_1
β : Type ?u.151825
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋
F : Type ?u.151819
α : Type u_1
β : Type ?u.151825
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ fract a + fract b ≤ fract (a + b) + 1
rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left]
no goals
F : Type ?u.151819
α : Type u_1
β : Type ?u.151825
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋
exact_mod_cast le_floor_add_floor a b