--- a/src/HOL/Arith.ML Thu Jan 09 10:22:11 1997 +0100
+++ b/src/HOL/Arith.ML Thu Jan 09 10:22:42 1997 +0100
@@ -475,6 +475,15 @@
by (fast_tac (!claset addDs [Suc_leD]) 1);
qed_spec_mp "add_leD1";
+goal Arith.thy "!!n::nat. m+k<=n ==> k<=n";
+by (full_simp_tac (!simpset addsimps [add_commute]) 1);
+by (etac add_leD1 1);
+qed_spec_mp "add_leD2";
+
+goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
+by (fast_tac (!claset addDs [add_leD1, add_leD2]) 1);
+bind_thm ("add_leE", result() RS conjE);
+
goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
by (safe_tac (!claset addSDs [less_eq_Suc_add]));
by (asm_full_simp_tac