# HG changeset patch
# User paulson
# Date 1677103286 0
# Node ID c6e2c7887d4700f2ca1561832a4ab7956ea7e48f
# Parent  c1c6f895d9ec501dd60ffbec4185a60d6087a5f9# Parent  a03bb622517c15f0b027dce1ec4cde841502f7fa
merged

diff -r c1c6f895d9ec -r c6e2c7887d47 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Feb 22 21:40:32 2023 +0100
+++ b/src/HOL/Int.thy	Wed Feb 22 22:01:26 2023 +0000
@@ -1754,6 +1754,9 @@
 lemma power_int_minus: "power_int (x::'a) (-n) = inverse (power_int x n)"
   by (auto simp: power_int_def power_inverse)
 
+lemma power_int_minus_divide: "power_int (x::'a) (-n) = 1 / (power_int x n)"
+  by (simp add: divide_inverse power_int_minus)
+
 lemma power_int_eq_0_iff [simp]: "power_int (x::'a) n = 0 \<longleftrightarrow> x = 0 \<and> n \<noteq> 0"
   by (auto simp: power_int_def)