no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : LimZero f
hg : LimZero g
⊢ LimZero (f - g)
simpa only [sub_eq_add_neg] using add_limZero hf (neg_limZero hg)