F : Type ?u.281474
α : Type u_1
β : Type ?u.281480
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x ∈ Ico (0 - 1 / 2) (1 - 1 / 2) ↔ x ∈ Ico (-(1 / 2)) (1 / 2)
F : Type ?u.281474
α : Type u_1
β : Type ?u.281480
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ round x = 0 ↔ x ∈ Ico (-(1 / 2)) (1 / 2)
rw [round_eq, floor_eq_zero_iff, add_mem_Ico_iff_left]
no goals
F : Type ?u.281474
α : Type u_1
β : Type ?u.281480
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x ∈ Ico (0 - 1 / 2) (1 - 1 / 2) ↔ x ∈ Ico (-(1 / 2)) (1 / 2)
norm_num