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