# HG changeset patch
# User paulson
# Date 931941611 -7200
# Node ID 8a1a39b8fad82ebf8b6bc4931db192d101ad6e9c
# Parent  1833bdd83ebfabdcd3174059ca37570bb21c0147
new montonicity theorems

diff -r 1833bdd83ebf -r 8a1a39b8fad8 src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Wed Jul 14 10:39:26 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Wed Jul 14 10:40:11 1999 +0200
@@ -81,9 +81,15 @@
 (*"v<=w ==> v+z <= w+z"*)
 bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
 
+(*"v<=w ==> z+v <= z+w"*)
+bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2);
+
 (*"v<=w ==> v+z <= w+z"*)
 bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
 
+(*"v<=w ==> z+v <= z+w"*)
+bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
+
 Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
 by (etac (zadd_zle_mono1 RS zle_trans) 1);
 by (Simp_tac 1);