src/HOL/Rational.thy

     using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq)
   show "(of_rat (Fract a b) :: 'a::ordered_field) < of_rat (Fract c d)
     \<longleftrightarrow> Fract a b < Fract c d"
     using not_zero `b * d > 0`
     by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
-      (auto intro: mult_strict_right_mono mult_right_less_imp_less)
 qed
 
 lemma of_rat_less_eq:
   "(of_rat r :: 'a::ordered_field) \<le> of_rat s \<longleftrightarrow> r \<le> s"
   unfolding le_less by (auto simp add: of_rat_less)