src/HOL/Analysis/Polytope.thy

     let ?n = "of_int (floor (x/a)) + 1"
     have x: "x < ?n * a"
       by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
     have "?n * a \<le> a + x"
       apply (simp add: algebra_simps)
-      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     also have "... < y"
       by (rule 1)
     finally have "?n * a < y" .
     with x show ?thesis
       using Ints_1 Ints_add Ints_of_int that by blast

     let ?n = "of_int (floor (y/a)) + 1"
     have y: "y < ?n * a"
       by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
     have "?n * a \<le> a + y"
       apply (simp add: algebra_simps)
-      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     also have "... < x"
       by (rule 2)
     finally have "?n * a < x" .
     then show ?thesis
       using Ints_1 Ints_add Ints_of_int that y by blast