no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hfg : LimZero (f - g)
⊢ LimZero (g - f)
simpa using neg_limZero hfg