# HG changeset patch
# User paulson
# Date 888934404 -3600
# Node ID 6efc56450d09532fd996c72f5774ccdcb49f2194
# Parent  248b876c2fa8d3b536b0ea56710694f5c4695e32
New theorem

diff -r 248b876c2fa8 -r 6efc56450d09 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Tue Mar 03 15:12:57 1998 +0100
+++ b/src/HOL/arith_data.ML	Tue Mar 03 15:13:24 1998 +0100
@@ -219,3 +219,16 @@
 
 context Arith.thy;
 Addsimprocs nat_cancel;
+
+
+(*This proof requires natdiff_cancel_sums*)
+goal Arith.thy "!!n::nat. m<n --> m<l --> (l-n) < (l-m)";
+by (induct_tac "l" 1);
+by (Simp_tac 1);
+by (Clarify_tac 1);
+be less_SucE 1;
+by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
+				      Suc_diff_n]) 1);
+by (Clarify_tac 1);
+by (asm_simp_tac (simpset() addsimps [less_imp_diff_is_0]) 1);
+qed_spec_mp "diff_less_mono2";