src/HOL/Analysis/Polytope.thy
changeset 64240 eabf80376aab
parent 63967 2aa42596edc3
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -2603,7 +2603,7 @@
     1.4        by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
     1.5      have "?n * a \<le> a + x"
     1.6        apply (simp add: algebra_simps)
     1.7 -      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     1.8 +      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
     1.9      also have "... < y"
    1.10        by (rule 1)
    1.11      finally have "?n * a < y" .
    1.12 @@ -2616,7 +2616,7 @@
    1.13        by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
    1.14      have "?n * a \<le> a + y"
    1.15        apply (simp add: algebra_simps)
    1.16 -      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
    1.17 +      by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
    1.18      also have "... < x"
    1.19        by (rule 2)
    1.20      finally have "?n * a < x" .