another fact on (- 1) ^ _

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