α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ LimZero (const abv (lim f) - f + (const abv (lim g) - g))
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ LimZero (const abv (lim f + lim g) - (f + g))
rw [const_add, add_sub_add_comm]
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f g : CauSeq β abv
⊢ LimZero (const abv (lim f) - f + (const abv (lim g) - g))
exact add_limZero (Setoid.symm (equiv_lim f)) (Setoid.symm (equiv_lim g))