--- 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"