tuned

--- a/src/HOL/Nat.thy	Tue Feb 18 19:59:42 2025 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 19 09:26:48 2025 +0100
@@ -1534,8 +1534,7 @@
 
 lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
   for f :: "'a \<Rightarrow> ('a::order)"
-  by (induct n arbitrary: A B)
-     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
+  by (induct n) (auto simp: mono_def)
 
 lemma funpow_mono2:
   assumes "mono f"