new theorem le_diff_conv

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