no goals
α : Type u_2
inst✝² : LinearOrderedField α
β : Type u_1
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : LimZero (const abv 0) then 0 else inv (const abv 0) h) = const abv 0
rw [dif_pos] <;> [rfl; exact zero_limZero]