1.1 --- a/src/ZF/Arith.ML	Wed Aug 19 10:34:31 1998 +0200
     1.2 +++ b/src/ZF/Arith.ML	Wed Aug 19 10:37:07 1998 +0200
     1.3 @@ -272,6 +272,13 @@
     1.4  by (ALLGOALS Asm_simp_tac);
     1.5  qed "diff_succ";
     1.6  
     1.7 +Goal "[| m: nat; n: nat |] ==> 0 < n #- m  <->  m<n";
     1.8 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
     1.9 +by (ALLGOALS Asm_simp_tac);
    1.10 +qed "zero_less_diff";
    1.11 +Addsimps [zero_less_diff];
    1.12 +
    1.13 +
    1.14  (** Subtraction is the inverse of addition. **)
    1.15  
    1.16  val [mnat,nnat] = goal Arith.thy