summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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 =