no goals
α : Type ?u.201083
β : Type ?u.201086
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx : x ≠ 0
⊢ ¬LimZero (const abv x)
rwa [const_limZero]