src/HOL/OrderedGroup.thy
changeset 29886 b8a6b9c56fdd
parent 29833 409138c4de12
child 29904 856f16a3b436
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Feb 12 20:36:41 2009 -0800
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Feb 12 21:24:14 2009 -0800
     1.3 @@ -478,6 +478,26 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma add_nonneg_eq_0_iff:
     1.8 +  assumes x: "0 \<le> x" and y: "0 \<le> y"
     1.9 +  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    1.10 +proof (intro iffI conjI)
    1.11 +  have "x = x + 0" by simp
    1.12 +  also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
    1.13 +  also assume "x + y = 0"
    1.14 +  also have "0 \<le> x" using x .
    1.15 +  finally show "x = 0" .
    1.16 +next
    1.17 +  have "y = 0 + y" by simp
    1.18 +  also have "0 + y \<le> x + y" using x by (rule add_right_mono)
    1.19 +  also assume "x + y = 0"
    1.20 +  also have "0 \<le> y" using y .
    1.21 +  finally show "y = 0" .
    1.22 +next
    1.23 +  assume "x = 0 \<and> y = 0"
    1.24 +  then show "x + y = 0" by simp
    1.25 +qed
    1.26 +
    1.27  end
    1.28  
    1.29  class pordered_ab_group_add =