# HG changeset patch
# User paulson
# Date 903428649 -7200
# Node ID 1003ddc302999f022a7fbfce28d99be1799cdac1
# Parent  ac539483ad09f45d3e91b104a0c0d93782dfa391
new theorem diff_Suc_less_diff

diff -r ac539483ad09 -r 1003ddc30299 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Aug 17 20:32:24 1998 +0200
+++ b/src/HOL/Arith.ML	Tue Aug 18 10:24:09 1998 +0200
@@ -369,6 +369,12 @@
 qed "diff_Suc_less";
 Addsimps [diff_Suc_less];
 
+Goal "i<n ==> n - Suc i < n - i";
+by (exhaust_tac "n" 1);
+by Safe_tac;
+by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1);
+qed "diff_Suc_less_diff";
+
 Goal "!!n::nat. m - n <= Suc m - n";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);