src/HOL/Integ/Int.thy

      "[| i \<le> j;  k \<le> l;  (0::int) \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*l"
   by (rule mult_mono)
 
 lemma zmult_zless_mono1: "[| i<j;  (0::int) < k |] ==> i*k < j*k"
   by (rule Ring_and_Field.mult_strict_right_mono)
-
-(* < monotonicity, BOTH arguments*)
-lemma zmult_zless_mono:
-     "[| i < j;  k < l;  (0::int) < j;  (0::int) < k |] ==> i*k < j*l"
-  by (rule Ring_and_Field.mult_strict_mono)
 
 lemma zmult_zless_mono1_neg: "[| i<j;  k < (0::int) |] ==> j*k < i*k"
   by (rule Ring_and_Field.mult_strict_right_mono_neg)
 
 lemma zmult_zless_mono2_neg: "[| i<j;  k < (0::int) |] ==> k*j < k*i"

 val zmult_zle_mono2 = thm "zmult_zle_mono2";
 val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
 val zmult_zle_mono = thm "zmult_zle_mono";
 val zmult_zless_mono2 = thm "zmult_zless_mono2";
 val zmult_zless_mono1 = thm "zmult_zless_mono1";
-val zmult_zless_mono = thm "zmult_zless_mono";
 val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
 val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
 val zmult_eq_0_iff = thm "zmult_eq_0_iff";
 val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
 val zmult_zless_cancel1 = thm "zmult_zless_cancel1";