# HG changeset patch
# User paulson
# Date 903515827 -7200
# Node ID eb105c6931a48048520fefd241ba3ff8be70c410
# Parent  d75c03cf77b5d745b86a04e7041b5fc1848010b1
new theorem zero_less_diff

diff -r d75c03cf77b5 -r eb105c6931a4 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Wed Aug 19 10:34:31 1998 +0200
+++ b/src/ZF/Arith.ML	Wed Aug 19 10:37:07 1998 +0200
@@ -272,6 +272,13 @@
 by (ALLGOALS Asm_simp_tac);
 qed "diff_succ";
 
+Goal "[| m: nat; n: nat |] ==> 0 < n #- m  <->  m<n";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "zero_less_diff";
+Addsimps [zero_less_diff];
+
+
 (** Subtraction is the inverse of addition. **)
 
 val [mnat,nnat] = goal Arith.thy