# HG changeset patch
# User paulson
# Date 931768350 -7200
# Node ID 52f70b76a8b509cb4e247e1df6d39b3a99ab1fc4
# Parent  3ae2eeabde80a825c0a0930f0d7632e3e50c6c8a
new theorems for the "at most" relation

diff -r 3ae2eeabde80 -r 52f70b76a8b5 src/HOL/Integ/Bin.ML
--- 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";