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