∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s : Finset ι} [AddLeftStrictMono M], (∀ i ∈ s, f i < 0) → s.Nonempty → ∑ i ∈ s, f i < 0