# HG changeset patch
# User bulwahn
# Date 1503808021 -7200
# Node ID 2b49d4888cb8d4bc54f1f1458eafb9262ada3673
# Parent  e5b1d4d55bf623897da7425cb3e9b0625a883c64
another fact on (- 1) ^ _

diff -r e5b1d4d55bf6 -r 2b49d4888cb8 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Aug 31 21:48:03 2017 +0200
+++ b/src/HOL/Parity.thy	Sun Aug 27 06:27:01 2017 +0200
@@ -242,6 +242,9 @@
 lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   by simp
 
+lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
+  by (cases "even (n + k)") auto
+
 end
 
 context linordered_idom