# HG changeset patch
# User paulson
# Date 852801762 -3600
# Node ID 7914881f47c0f16782de556ccf0478df53fc323a
# Parent  47de509bdd55432b1a89ab7081d879704972cf2f
New theorem add_leE

diff -r 47de509bdd55 -r 7914881f47c0 src/HOL/Arith.ML
--- 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