src/HOL/Multivariate_Analysis/Linear_Algebra.thy

       using fS SP vS by auto
     have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =
       setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
       using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps)
     also have "\<dots> = ?a"
-      unfolding scaleR_right.setsum [symmetric] u using uv by (simp add: divide_minus_left)
+      unfolding scaleR_right.setsum [symmetric] u using uv by simp
     finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
     with th0 have ?lhs
       unfolding dependent_def span_explicit
       apply -
       apply (rule bexI[where x= "?a"])

       by blast
   next
     case False
     with span_mul[OF th, of "- 1/ k"]
     have th1: "f a \<in> span (f ` b)"
-      by (auto simp: divide_minus_left)
+      by auto
     from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
     have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
     from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
     have "f a \<notin> span (f ` b)" using tha
       using "2.hyps"(2)