# HG changeset patch
# User nipkow
# Date 1238597731 -7200
# Node ID bf99ceb7d01537a8a8f860eab600f8a73d335a03
# Parent  d09a0794d4571c8b6eee016a3666e120e811e466
added setsum_pos_nat

diff -r d09a0794d457 -r bf99ceb7d015 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Apr 01 16:03:18 2009 +0200
+++ b/src/HOL/Int.thy	Wed Apr 01 16:55:31 2009 +0200
@@ -1408,6 +1408,10 @@
     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
   by (rule setprod_nonzero, auto)
 
+lemma setprod_pos_nat:
+  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
+using setprod_nonzero_nat by simp
+
 lemma setprod_zero_eq_nat:
     "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
   by (rule setprod_zero_eq, auto)