F : Type ?u.150574
α : Type u_1
β : Type ?u.150580
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
F : Type ?u.150574
α : Type u_1
β : Type ?u.150580
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ fract (a + b) ≤ fract a + fract b
rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ← Int.cast_add, Int.cast_le]
no goals
F : Type ?u.150574
α : Type u_1
β : Type ?u.150580
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
exact le_floor_add _ _