# 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 ==> (\x \ A. f x \ (0::nat)) ==> setprod f A \ 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)) = (\x \ A. f x = 0)" by (rule setprod_zero_eq, auto)