# HG changeset patch
# User haftmann
# Date 1240926630 -7200
# Node ID e1309df633c648eeefe804ff70df8cdb109d14e4
# Parent  555f4033cd971bd4f0ba0de9194d8e3d56844ff7
lemma sum_nonneg_eq_zero_iff

diff -r 555f4033cd97 -r e1309df633c6 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Tue Apr 28 15:50:29 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -637,6 +637,27 @@
 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