F : Type ?u.166631
α : Type u_1
β : Type ?u.166637
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b - ↑⌊a + b⌋ - (a - ↑⌊a⌋) - (b - ↑⌊b⌋) = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)
F : Type ?u.166631
α : Type u_1
β : Type ?u.166637
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ fract (a + b) - fract a - fract b = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)
unfold fract
F : Type ?u.166631
α : Type u_1
β : Type ?u.166637
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b + -↑⌊a + b⌋ + (↑⌊a⌋ + -a) + (↑⌊b⌋ + -b) = ↑⌊a⌋ + ↑⌊b⌋ + -↑⌊a + b⌋
F : Type ?u.166631
α : Type u_1
β : Type ?u.166637
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b - ↑⌊a + b⌋ - (a - ↑⌊a⌋) - (b - ↑⌊b⌋) = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)
simp [sub_eq_add_neg]
no goals
F : Type ?u.166631
α : Type u_1
β : Type ?u.166637
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a b : α
⊢ a + b + -↑⌊a + b⌋ + (↑⌊a⌋ + -a) + (↑⌊b⌋ + -b) = ↑⌊a⌋ + ↑⌊b⌋ + -↑⌊a + b⌋
abel