--- a/src/HOL/Integ/Bin.ML Mon Jul 12 10:02:38 1999 +0200
+++ b/src/HOL/Integ/Bin.ML Mon Jul 12 10:32:30 1999 +0200
@@ -746,3 +746,25 @@
by (force_tac (claset() addDs [zmult_zless_mono1],
simpset() addsimps [order_le_less]) 1);
qed "pos_imp_zmult_pos_iff";
+
+(** <= versions of the theorems above **)
+
+Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)";
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ neg_imp_zmult_pos_iff]) 1);
+qed "neg_imp_zmult_nonpos_iff";
+
+Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)";
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ neg_imp_zmult_neg_iff]) 1);
+qed "neg_imp_zmult_nonneg_iff";
+
+Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)";
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ pos_imp_zmult_pos_iff]) 1);
+qed "pos_imp_zmult_nonpos_iff";
+
+Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)";
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ pos_imp_zmult_neg_iff]) 1);
+qed "pos_imp_zmult_nonneg_iff";