changeset 5485 | 0cd451e46a20 |
parent 5429 | 0833486c23ce |
child 5497 | 497215d66441 |
--- 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";