F : Type ?u.257064
α : Type u_1
β : Type ?u.257070
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (x + -↑↑y) = round x - ↑y
F : Type ?u.257064
α : Type u_1
β : Type ?u.257070
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (x - ↑y) = round x - ↑y
rw [sub_eq_add_neg, ← Int.cast_ofNat]
F : Type ?u.257064
α : Type u_1
β : Type ?u.257070
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (x + ↑(-↑y)) = round x - ↑y
F : Type ?u.257064
α : Type u_1
β : Type ?u.257070
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (x + -↑↑y) = round x - ↑y
norm_cast
no goals
F : Type ?u.257064
α : Type u_1
β : Type ?u.257070
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (x + ↑(-↑y)) = round x - ↑y
rw [round_add_int, sub_eq_add_neg]