src/HOL/Multivariate_Analysis/Integration.thy

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -222,6 +222,9 @@
 lemma empty_as_interval: "{} = {One..(0::'a::ordered_euclidean_space)}"
   by (auto simp: eucl_le[where 'a='a])
 
+lemma One_nonneg: "0 \<le> (One::'a::ordered_euclidean_space)"
+  by (auto intro: setsum_nonneg)
+
 lemma interior_subset_union_intervals:
   assumes "i = {a..b::'a::ordered_euclidean_space}"
     and "j = {c..d}"