# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1677079456 0
# Node ID a03bb622517c15f0b027dce1ec4cde841502f7fa
# Parent  505958b16880944a6613636ecfcf910144f88d27
One new (necessary) theorem

diff -r 505958b16880 -r a03bb622517c src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Feb 21 16:47:03 2023 +0000
+++ b/src/HOL/Int.thy	Wed Feb 22 15:24:16 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)