# HG changeset patch
# User huffman
# Date 1272329799 25200
# Node ID 1c0f42fb92f1d2dd63931e81e0785fdee09225ef
# Parent  bbe2730e6db6dd9fac8ce810a7a9aa9dcd3e88b5
remove redundant lemma

diff -r bbe2730e6db6 -r 1c0f42fb92f1 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 26 16:28:58 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 26 17:56:39 2010 -0700
@@ -599,19 +599,6 @@
 
 end
 
-lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"
-using fS fp setsum_nonneg[OF fp]
-proof (induct set: finite)
-  case empty thus ?case by simp
-next
-  case (insert x F)
-  from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all
-  from insert.hyps Fp setsum_nonneg[OF Fp]
-  have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis
-  from add_nonneg_eq_0_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
-  show ?case by (simp add: h)
-qed
-
 subsection {* A connectedness or intermediate value lemma with several applications. *}
 
 lemma connected_real_lemma: