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