src/HOL/Computational_Algebra/Polynomial.thy

   by (metis less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos)
 
 lemma poly_MVT: "a < b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p b - poly p a = (b - a) * poly (pderiv p) x"
   for a b :: real
   using MVT [of a b "poly p"]
-  apply auto
-  apply (rule_tac x = z in exI)
-  apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
-  done
+  apply simp
+  by (metis (full_types) DERIV_continuous_on DERIV_unique has_field_derivative_at_within poly_DERIV)
 
 lemma poly_MVT':
   fixes a b :: real
   assumes "{min a b..max a b} \<subseteq> A"
   shows "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) x"