new theorem zero_less_diff

--- 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