src/HOL/Library/Float.thy

--- a/src/HOL/Library/Float.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Library/Float.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -1816,7 +1816,7 @@
   assumes "b > 0"
   shows "a \<ge> b * (a div b)"
 proof -
-  from zmod_zdiv_equality'[of a b] have "a = b * (a div b) + a mod b"
+  from minus_div_mult_eq_mod [symmetric, of a b] have "a = b * (a div b) + a mod b"
     by simp
   also have "\<dots> \<ge> b * (a div b) + 0"
     apply (rule add_left_mono)