src/HOL/OrderedGroup.thy
changeset 31034 736f521ad036
parent 31016 e1309df633c6
child 31902 862ae16a799d
     1.1 --- a/src/HOL/OrderedGroup.thy	Mon May 04 14:49:48 2009 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon May 04 14:49:49 2009 +0200
     1.3 @@ -637,27 +637,6 @@
     1.4  lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
     1.5  by (simp add: algebra_simps)
     1.6  
     1.7 -lemma sum_nonneg_eq_zero_iff:
     1.8 -  assumes x: "0 \<le> x" and y: "0 \<le> y"
     1.9 -  shows "(x + y = 0) = (x = 0 \<and> y = 0)"
    1.10 -proof -
    1.11 -  have "x + y = 0 \<Longrightarrow> x = 0"
    1.12 -  proof -
    1.13 -    from y have "x + 0 \<le> x + y" by (rule add_left_mono)
    1.14 -    also assume "x + y = 0"
    1.15 -    finally have "x \<le> 0" by simp
    1.16 -    then show "x = 0" using x by (rule antisym)
    1.17 -  qed
    1.18 -  moreover have "x + y = 0 \<Longrightarrow> y = 0"
    1.19 -  proof -
    1.20 -    from x have "0 + y \<le> x + y" by (rule add_right_mono)
    1.21 -    also assume "x + y = 0"
    1.22 -    finally have "y \<le> 0" by simp
    1.23 -    then show "y = 0" using y by (rule antisym)
    1.24 -  qed
    1.25 -  ultimately show ?thesis by auto
    1.26 -qed
    1.27 -
    1.28  text{*Legacy - use @{text algebra_simps} *}
    1.29  lemmas group_simps[noatp] = algebra_simps
    1.30