--- 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"