# HG changeset patch
# User nipkow
# Date 1101196712 -3600
# Node ID 56c830f91b3885423173bc4e6d98b81e36b6a0c4
# Parent  10dd989282fdebf3d11a169a82ee36bb685e5570
added lemma

diff -r 10dd989282fd -r 56c830f91b38 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Nov 22 13:52:27 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 23 08:58:32 2004 +0100
@@ -1015,6 +1015,14 @@
   apply (blast intro: add_mono)
   done
 
+lemma setsum_nonpos: "[| finite A;
+    \<forall>x \<in> A. f x \<le> (0::'a::ordered_semidom) |] ==>
+    setsum f A \<le> 0";
+  apply (induct set: Finites, auto)
+  apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)
+  apply (blast intro: add_mono)
+  done
+
 lemma setsum_mult: 
   fixes f :: "'a => ('b::semiring_0_cancel)"
   assumes fin: "finite A"