no goals
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
⊢ (if h : LimZero f then 0 else inv f h) = inv f hf
rw [dif_neg]