# HG changeset patch
# User nipkow
# Date 803817869 -7200
# Node ID b6e1e74695f6582e977f080eecde79616c7e3c2d
# Parent  c820b3cc3df09a142862d8b7d62684f23e9843af
Added add_lessD1

diff -r c820b3cc3df0 -r b6e1e74695f6 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Jun 21 15:47:10 1995 +0200
+++ b/src/HOL/Arith.ML	Thu Jun 22 12:44:29 1995 +0200
@@ -303,6 +303,13 @@
 (*"i < j ==> i < m+j"*)
 bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
 
+goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
+be rev_mp 1;
+by(nat_ind_tac "j" 1);
+by (ALLGOALS(asm_simp_tac arith_ss));
+by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+qed "add_lessD1";
+
 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
 by (eresolve_tac [le_trans] 1);
 by (resolve_tac [le_add1] 1);