# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1596646593 -3600
# Node ID beccb2a0410f00e35d227dea8043a786a00d6a5d
# Parent  6a2f439013507cf9c6ee4aa6348b8aa0dc5ac0a1
yet another little lemma

diff -r 6a2f43901350 -r beccb2a0410f src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Aug 05 17:50:00 2020 +0100
+++ b/src/HOL/Groups_Big.thy	Wed Aug 05 17:56:33 2020 +0100
@@ -1070,6 +1070,21 @@
   finally show ?thesis .
 qed
 
+lemma sum_strict_mono2:
+  fixes f :: "'a \<Rightarrow> 'b::ordered_cancel_comm_monoid_add"
+  assumes "finite B" "A \<subseteq> B" "b \<in> B-A" "f b > 0" and "\<And>x. x \<in> B \<Longrightarrow> f x \<ge> 0"
+  shows "sum f A < sum f B"
+proof -
+  have "B - A \<noteq> {}"
+    using assms(3) by blast
+  have "sum f (B-A) > 0"
+    by (rule sum_pos2) (use assms in auto)
+  moreover have "sum f B = sum f (B-A) + sum f A"
+    by (rule sum.subset_diff) (use assms in auto)
+  ultimately show ?thesis
+    using add_strict_increasing by auto
+qed
+
 lemma sum_cong_Suc:
   assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)"
   shows "sum f A = sum g A"