--- 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 **)