F : Type ?u.255284
α : Type u_1
β : Type ?u.255290
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + -↑y) = round x - y
F : Type ?u.255284
α : Type u_1
β : Type ?u.255290
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x - ↑y) = round x - y
rw [sub_eq_add_neg]
F : Type ?u.255284
α : Type u_1
β : Type ?u.255290
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑(-y)) = round x - y
F : Type ?u.255284
α : Type u_1
β : Type ?u.255290
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + -↑y) = round x - y
norm_cast
no goals
F : Type ?u.255284
α : Type u_1
β : Type ?u.255290
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑(-y)) = round x - y
rw [round_add_int, sub_eq_add_neg]