changeset 36977 | 71c8973a604b |
parent 36348 | 89c54f51f55a |
child 37884 | 314a88278715 |
--- a/src/HOL/Groups.thy Mon May 17 18:51:25 2010 -0700 +++ b/src/HOL/Groups.thy Mon May 17 18:59:59 2010 -0700 @@ -605,7 +605,7 @@ then show ?thesis by simp qed -lemma add_nonneg_nonneg: +lemma add_nonneg_nonneg [simp]: assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b" proof - have "0 + 0 \<le> a + b"