∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] (f : α → β),
  (∀ (a b : α), f (a + b) ≤ f a + f b) → ∀ (l : List α), l ≠ ∅ → f l.sum ≤ (List.map f l).sum