summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Thu, 12 Feb 2009 21:24:14 -0800 | |

changeset 29886 | b8a6b9c56fdd |

parent 29885 | 379e43e513c2 |

child 29887 | 5170d6277b61 |

child 29888 | ab97183f1694 |

add lemma add_nonneg_eq_0_iff

--- 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 =