diff -r 34023a586608 -r aefb4a8da31f src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -446,7 +446,6 @@
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
 apply (simp add: power2_sum x y)
-apply (simp add: mult_nonneg_nonneg x y)
 apply (simp add: x y)
 done