# HG changeset patch
# User paulson
# Date 904637351 -7200
# Node ID e97558ee8e76c00b5dc406e5ee1da9d13fceef37
# Parent  0a0a35dddabdb407e146f7ef2d474dbfd6d19f52
Two new subtraction lemmas

diff -r 0a0a35dddabd -r e97558ee8e76 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Sun Aug 30 15:14:42 1998 +0200
+++ b/src/HOL/Arith.ML	Tue Sep 01 10:09:11 1998 +0200
@@ -493,6 +493,7 @@
 qed "diff_add_0";
 Addsimps [diff_add_0];
 
+
 (** Difference distributes over multiplication **)
 
 Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
@@ -675,6 +676,17 @@
 qed "diff_Suc_le_diff";
 AddIffs [diff_Suc_le_diff];
 
+Goal "0 < n ==> (m <= n-1) = (m<n)";
+by (exhaust_tac "n" 1);
+by Auto_tac;
+by (ALLGOALS trans_tac);
+qed "le_pred_eq";
+
+Goal "0 < n ==> (m-1 < n) = (m<=n)";
+by (exhaust_tac "m" 1);
+by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
+qed "less_pred_eq";
+
 
 
 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)