tuned proof: avoid z3 to make it work on arm64-linux;

--- a/src/HOL/ex/BigO.thy	Wed Jan 31 16:55:16 2024 +0100
+++ b/src/HOL/ex/BigO.thy	Wed Jan 31 19:17:45 2024 +0100
@@ -271,7 +271,7 @@
   by (metis equalityI bigo_const2 bigo_const4)
 
 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
-  by (smt (z3) abs_mult bigo_def bigo_refl mem_Collect_eq mult.left_commute mult_commute_abs)
+  by (simp add: bigo_def) (metis abs_mult dual_order.refl)
 
 lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
   by (metis bigo_elt_subset bigo_const_mult1)