no goals
F : Type ?u.256390
α : Type u_1
β : Type ?u.256396
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (x + ↑y) = round x + ↑y
rw [round, round, fract_add_nat, Int.floor_add_nat, Int.ceil_add_nat, ← apply_ite₂, ite_self]