src/HOL/Multivariate_Analysis/Linear_Algebra.thy

     and z: "0 \<le> z"
     and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
   shows "x \<le> y + z"
 proof -
   have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
-    using z y by (simp add: mult_nonneg_nonneg)
+    using z y by simp
   with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
     by (simp add: power2_eq_square field_simps)
   from y z have yz: "y + z \<ge> 0"
     by arith
   from power2_le_imp_le[OF th yz] show ?thesis .