# HG changeset patch
# User paulson
# Date 906124166 -7200
# Node ID 739b777e435511a32c95c7a7d6f1dcbe7b4ee35c
# Parent  613a42644c2e56e40cc519b275342cb893c4076d
new theorem less_imp_Suc_add

diff -r 613a42644c2e -r 739b777e4355 src/ZF/Arith.ML
--- 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";