--- a/src/HOL/Groups_Big.thy Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Groups_Big.thy Wed Jun 18 07:31:12 2014 +0200
@@ -1317,4 +1317,8 @@
"finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
+lemma (in ordered_comm_monoid_add) setsum_pos:
+ "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
+ by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
+
end