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