1.1 --- a/src/HOL/Arith.ML	Mon Aug 17 20:32:24 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Tue Aug 18 10:24:09 1998 +0200
     1.3 @@ -369,6 +369,12 @@
     1.4  qed "diff_Suc_less";
     1.5  Addsimps [diff_Suc_less];
     1.6  
     1.7 +Goal "i<n ==> n - Suc i < n - i";
     1.8 +by (exhaust_tac "n" 1);
     1.9 +by Safe_tac;
    1.10 +by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1);
    1.11 +qed "diff_Suc_less_diff";
    1.12 +
    1.13  Goal "!!n::nat. m - n <= Suc m - n";
    1.14  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.15  by (ALLGOALS Asm_simp_tac);