F : Type ?u.147946
α : Type u_1
β : Type ?u.147952
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a
F : Type ?u.147946
α : Type u_1
β : Type ?u.147952
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
m : ℤ
⊢ fract (a - ↑m) = fract a
rw [fract]
no goals
F : Type ?u.147946
α : Type u_1
β : Type ?u.147952
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a
simp