F : Type ?u.172838
α : Type u_1
β : Type ?u.172844
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a x : α
⊢ (∃ z, -x = ↑z) ↔ ∃ z, x = ↑z
F : Type ?u.172838
α : Type u_1
β : Type ?u.172844
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a x : α
⊢ fract (-x) = 0 ↔ fract x = 0
simp only [fract_eq_iff, le_refl, zero_lt_one, tsub_zero, true_and_iff]
no goals
F : Type ?u.172838
α : Type u_1
β : Type ?u.172844
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a x : α
⊢ (∃ z, -x = ↑z) ↔ ∃ z, x = ↑z
constructor <;> rintro ⟨z, hz⟩ <;> use -z <;> simp [← hz]