# HG changeset patch
# User huffman
# Date 1234502654 28800
# Node ID b8a6b9c56fddc55286c480f8f639b14351185558
# Parent  379e43e513c21e3ee8967161603d646e86fd3de2
add lemma add_nonneg_eq_0_iff

diff -r 379e43e513c2 -r b8a6b9c56fdd src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Thu Feb 12 20:36:41 2009 -0800
+++ b/src/HOL/OrderedGroup.thy	Thu Feb 12 21:24:14 2009 -0800
@@ -478,6 +478,26 @@
   then show ?thesis by simp
 qed
 
+lemma add_nonneg_eq_0_iff:
+  assumes x: "0 \<le> x" and y: "0 \<le> y"
+  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+proof (intro iffI conjI)
+  have "x = x + 0" by simp
+  also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
+  also assume "x + y = 0"
+  also have "0 \<le> x" using x .
+  finally show "x = 0" .
+next
+  have "y = 0 + y" by simp
+  also have "0 + y \<le> x + y" using x by (rule add_right_mono)
+  also assume "x + y = 0"
+  also have "0 \<le> y" using y .
+  finally show "y = 0" .
+next
+  assume "x = 0 \<and> y = 0"
+  then show "x + y = 0" by simp
+qed
+
 end
 
 class pordered_ab_group_add =