diff -r 048bbe0bf807 -r 1d2222800ecd src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sat Jul 23 12:19:45 2022 +0200
+++ b/src/HOL/Groups_List.thy	Mon Jul 25 12:19:59 2022 +0200
@@ -252,6 +252,15 @@
   qed
 qed
 
+text \<open>A much more general version of this monotonicity lemma
+can be formulated with multisets and the multiset order\<close>
+
+lemma sum_list_mono2: fixes xs :: "'a ::ordered_comm_monoid_add list"
+shows "\<lbrakk> length xs = length ys; \<And>i. i < length xs \<longrightarrow> xs!i \<le> ys!i \<rbrakk>
+  \<Longrightarrow> sum_list xs \<le> sum_list ys"
+apply(induction xs ys rule: list_induct2)
+by(auto simp: nth_Cons' less_Suc_eq_0_disj imp_ex add_mono)
+
 lemma (in monoid_add) sum_list_distinct_conv_sum_set:
   "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)"
   by (induct xs) simp_all