# HG changeset patch
# User nipkow
# Date 1538809145 -7200
# Node ID 4596b580d1dd85afdc660c45f8e3e21e14652735
# Parent  e1b4b14ded5833451b41ca34c627a61d024678ac
generalization due to Alexander Maletzky

diff -r e1b4b14ded58 -r 4596b580d1dd src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Oct 05 23:49:12 2018 +0200
+++ b/src/HOL/Groups_Big.thy	Sat Oct 06 08:59:05 2018 +0200
@@ -1427,7 +1427,7 @@
 qed
 
 lemma sum_image_le:
-  fixes g :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
+  fixes g :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)"
     shows "sum g (f ` I) \<le> sum (g \<circ> f) I"
   using assms
@@ -1435,12 +1435,14 @@
   case empty
   then show ?case by auto
 next
-  case (insert x F) then
+  case (insert x F)
+  from insertI1 have "0 \<le> g (f x)" by (rule insert)
+  hence 1: "sum g (f ` F) \<le> g (f x) + sum g (f ` F)" using add_increasing by blast
+  have 2: "sum g (f ` F) \<le> sum (g \<circ> f) F" using insert by blast
   have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp
-  also have "\<dots> \<le> g (f x) + sum g (f ` F)"
-    by (simp add: insert sum.insert_if)
-  also have "\<dots>  \<le> sum (g \<circ> f) (insert x F)"
-    using insert by auto
+  also have "\<dots> \<le> g (f x) + sum g (f ` F)" by (simp add: 1 insert sum.insert_if)
+  also from 2 have "\<dots> \<le> g (f x) + sum (g \<circ> f) F" by (rule add_left_mono)
+  also from insert(1, 2) have "\<dots> = sum (g \<circ> f) (insert x F)" by (simp add: sum.insert_if)
   finally show ?case .
 qed