# HG changeset patch
# User paulson
# Date 905761039 -7200
# Node ID 0cd451e46a200bc1d39c3602644191c70fabed33
# Parent  e9430ed7e8d6986dc66489a3a70b2330cddfcdd5
new theorem le_diff_conv

diff -r e9430ed7e8d6 -r 0cd451e46a20 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Sep 11 18:09:54 1998 +0200
+++ b/src/HOL/Arith.ML	Mon Sep 14 10:17:19 1998 +0200
@@ -633,6 +633,11 @@
 be add_less_imp_less_diff 1;
 qed "less_diff_conv";
 
+Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
+by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc, less_diff_conv,
+					   Suc_diff_le RS sym]) 1);
+qed "le_diff_conv";
+
 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
 by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
 qed "Suc_diff_Suc";