src/HOL/Series.thy

   have finite_S1: "\<And>n. finite (?S1 n)" by simp
   with S2_le_S1 have finite_S2: "\<And>n. finite (?S2 n)" by (rule finite_subset)
 
   let ?g = "\<lambda>(i,j). a i * b j"
   let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)"
-  have f_nonneg: "\<And>x. 0 \<le> ?f x"
-    by (auto simp add: mult_nonneg_nonneg)
+  have f_nonneg: "\<And>x. 0 \<le> ?f x" by (auto)
   hence norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A"
     unfolding real_norm_def
     by (simp only: abs_of_nonneg setsum_nonneg [rule_format])
 
   have "(\<lambda>n. (\<Sum>k<n. a k) * (\<Sum>k<n. b k)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"