# HG changeset patch
# User haftmann
# Date 1241441389 -7200
# Node ID 736f521ad0364e82527b0db5dd5b0b6acb110407
# Parent  c46d52fee219e395c94c57c3925a4c6682c64388
dropped duplicate lemma sum_nonneg_eq_zero_iff

diff -r c46d52fee219 -r 736f521ad036 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon May 04 14:49:48 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon May 04 14:49:49 2009 +0200
@@ -593,7 +593,7 @@
   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 sum_nonneg_eq_zero_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
+  from add_nonneg_eq_0_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
   show ?case by (simp add: h)
 qed
 
diff -r c46d52fee219 -r 736f521ad036 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Mon May 04 14:49:48 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy	Mon May 04 14:49:49 2009 +0200
@@ -127,7 +127,7 @@
 
 lemma sum_squares_eq_zero_iff:
   "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
-  by (simp add: sum_nonneg_eq_zero_iff)
+  by (simp add: add_nonneg_eq_0_iff)
 
 lemma sum_squares_le_zero_iff:
   "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
diff -r c46d52fee219 -r 736f521ad036 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Mon May 04 14:49:48 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Mon May 04 14:49:49 2009 +0200
@@ -637,27 +637,6 @@
 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
 by (simp add: algebra_simps)
 
-lemma sum_nonneg_eq_zero_iff:
-  assumes x: "0 \<le> x" and y: "0 \<le> y"
-  shows "(x + y = 0) = (x = 0 \<and> y = 0)"
-proof -
-  have "x + y = 0 \<Longrightarrow> x = 0"
-  proof -
-    from y have "x + 0 \<le> x + y" by (rule add_left_mono)
-    also assume "x + y = 0"
-    finally have "x \<le> 0" by simp
-    then show "x = 0" using x by (rule antisym)
-  qed
-  moreover have "x + y = 0 \<Longrightarrow> y = 0"
-  proof -
-    from x have "0 + y \<le> x + y" by (rule add_right_mono)
-    also assume "x + y = 0"
-    finally have "y \<le> 0" by simp
-    then show "y = 0" using y by (rule antisym)
-  qed
-  ultimately show ?thesis by auto
-qed
-
 text{*Legacy - use @{text algebra_simps} *}
 lemmas group_simps[noatp] = algebra_simps