no goals
α : Type u_2
β : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ LimZero (const x - const y) ↔ x = y
rw [← const_sub, const_limZero, sub_eq_zero]