new theorem less_imp_Suc_add

--- a/src/ZF/Arith.ML	Fri Sep 18 15:08:46 1998 +0200
+++ b/src/ZF/Arith.ML	Fri Sep 18 15:09:26 1998 +0200
@@ -263,6 +263,12 @@
 by (ALLGOALS Asm_simp_tac);
 qed "add_diff_inverse";
 
+Goal "[| n le m;  m:nat |] ==> (m#-n) #+ n = m";
+by (forward_tac [lt_nat_in_nat] 1);
+by (etac nat_succI 1);
+by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
+qed "add_diff_inverse2";
+
 (*Proof is IDENTICAL to that above*)
 Goal "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)";
 by (forward_tac [lt_nat_in_nat] 1);
@@ -579,8 +585,7 @@
 
 
 (*Thanks to Sten Agerholm*)
-Goal  (* add_le_elim1 *)
-    "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
+Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
 by (etac rev_mp 1);
 by (eres_inst_tac [("n","n")] nat_induct 1);
 by (Asm_simp_tac 1);
@@ -593,3 +598,11 @@
 by (Blast_tac 1);
 qed "add_le_elim1";
 
+Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
+by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
+be rev_mp 1;
+by (etac nat_induct 1);
+by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
+by (blast_tac (claset() addSEs [leE] 
+                        addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
+qed_spec_mp "less_imp_Suc_add";