changeset 14387 | e96d5c42c4b0 |
parent 13871 | 26e5f5e624f6 |
child 14981 | e73f8140af78 |
--- a/src/HOL/NumberTheory/Int2.thy Sat Feb 14 02:06:12 2004 +0100 +++ b/src/HOL/NumberTheory/Int2.thy Sun Feb 15 10:46:37 2004 +0100 @@ -62,7 +62,7 @@ by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac) also assume "x < y * z"; finally show ?thesis; - by (auto simp add: prems zmult_zless_cancel2, insert prems, arith) + by (auto simp add: prems mult_less_cancel_right, insert prems, arith) qed; lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";