no goals
α : Type u_1
β : Type u_2
γ : Type ?u.406920
δ : Type ?u.406923
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
hfg : Summable fun b => f b - g b
hf : Summable f
⊢ Summable fun b => g b - f b
simpa only [neg_sub] using hfg.neg