src/ZF/Integ/Int.ML

--- a/src/ZF/Integ/Int.ML	Tue Jun 26 16:54:39 2001 +0200
+++ b/src/ZF/Integ/Int.ML	Tue Jun 26 17:04:09 2001 +0200
@@ -986,6 +986,29 @@
 Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
 
 
+(*"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 "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z";
+by (etac (zadd_zle_mono1 RS zle_trans) 1);
+by (Simp_tac 1);
+qed "zadd_zle_mono";
+
+Goal "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z";
+by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
+by (Simp_tac 1);
+qed "zadd_zless_mono";
+
+
 (*** Comparison laws ***)
 
 Goal "($- x $< $- y) <-> (y $< x)";