diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Int.thy	Mon Sep 25 17:06:05 2023 +0100
@@ -1738,6 +1738,12 @@
 lemma power_int_numeral [simp]: "power_int x (numeral n) = x ^ numeral n"
   by (simp add: power_int_def)
 
+lemma powi_numeral_reduce: "x powi numeral n = x * x powi int (pred_numeral n)"
+  by (simp add: numeral_eq_Suc)
+
+lemma powi_minus_numeral_reduce: "x powi - (numeral n) = inverse x * x powi - int(pred_numeral n)"
+  by (simp add: numeral_eq_Suc power_int_def)
+
 lemma int_cases4 [case_names nonneg neg]:
   fixes m :: int
   obtains n where "m = int n" | n where "n > 0" "m = -int n"