--- a/src/HOL/Analysis/Infinite_Sum.thy Sun Mar 03 12:28:22 2024 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy Sun Mar 03 16:18:06 2024 +0100
@@ -1961,7 +1961,7 @@
by (metis (no_types, lifting) b4 infsum_mono2 norm_ge_zero summable_on_subset_banach x2_sum)
have "norm (x i * y i) \<le> norm (x i * x i) + norm (y i * y i)" for i
- unfolding norm_mult by (smt mult_left_mono mult_nonneg_nonneg mult_right_mono norm_ge_zero)
+ unfolding norm_mult by (smt (verit, best) abs_norm_cancel mult_mono not_sum_squares_lt_zero)
hence "(\<Sum>i\<in>F. norm (x i * y i)) \<le> (\<Sum>i\<in>F. norm (x i * x i) + norm (y i * y i))"
by (simp add: sum_mono)
also have "\<dots> = (\<Sum>i\<in>F. norm (x i * x i)) + (\<Sum>i\<in>F. norm (y i * y i))"