src/ZF/ArithSimp.ML

--- a/src/ZF/ArithSimp.ML	Thu Sep 07 15:31:09 2000 +0200
+++ b/src/ZF/ArithSimp.ML	Thu Sep 07 17:36:37 2000 +0200
@@ -458,5 +458,6 @@
                         addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
 qed_spec_mp "less_imp_succ_add";
 
-
-
+Goal "[| m: nat; n: nat |] ==> (m<n) <-> (EX k: nat. n = succ(m#+k))";
+by (auto_tac (claset() addIs [less_imp_succ_add], simpset()));
+qed "less_iff_succ_add";