# HG changeset patch
# User haftmann
# Date 1197526140 -3600
# Node ID 314d949c70b553b71b410e4b774a8f533dc074e0
# Parent  c0deb73077322beb9c1fef1e084a02d04abb09f3
added lemma

diff -r c0deb7307732 -r 314d949c70b5 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Dec 13 07:08:59 2007 +0100
+++ b/src/HOL/Nat.thy	Thu Dec 13 07:09:00 2007 +0100
@@ -1443,6 +1443,13 @@
 text{*At present we prove no analogue of @{text not_less_Least} or @{text
 Least_Suc}, since there appears to be no need.*}
 
+text {* a nice rewrite for bounded subtraction *}
+
+lemma nat_minus_add_max:
+  fixes n m :: nat
+  shows "n - m + m = max n m"
+  by (simp add: max_def)
+
 
 subsection {*The Set of Natural Numbers*}