src/HOL/arith_data.ML
changeset 4675 6efc56450d09
parent 4368 1f2dd130fe39
child 5132 24f992a25adc
     1.1 --- a/src/HOL/arith_data.ML	Tue Mar 03 15:12:57 1998 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Tue Mar 03 15:13:24 1998 +0100
     1.3 @@ -219,3 +219,16 @@
     1.4  
     1.5  context Arith.thy;
     1.6  Addsimprocs nat_cancel;
     1.7 +
     1.8 +
     1.9 +(*This proof requires natdiff_cancel_sums*)
    1.10 +goal Arith.thy "!!n::nat. m<n --> m<l --> (l-n) < (l-m)";
    1.11 +by (induct_tac "l" 1);
    1.12 +by (Simp_tac 1);
    1.13 +by (Clarify_tac 1);
    1.14 +be less_SucE 1;
    1.15 +by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
    1.16 +				      Suc_diff_n]) 1);
    1.17 +by (Clarify_tac 1);
    1.18 +by (asm_simp_tac (simpset() addsimps [less_imp_diff_is_0]) 1);
    1.19 +qed_spec_mp "diff_less_mono2";