# HG changeset patch
# User wenzelm
# Date 1709479086 -3600
# Node ID f20ac6788faacc115648c06f9ac6e0a2f94b1e37
# Parent  444e409e6c6feead8c6715a70d4c8e11e33d57b8
tuned proof: avoid z3 to make it work on arm64-linux;

diff -r 444e409e6c6f -r f20ac6788faa src/HOL/Analysis/Infinite_Sum.thy
--- 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))"