∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f →
    Filter.Tendsto (fun x => f x + g x) l Filter.atTop → Filter.Tendsto g l Filter.atTop