src/HOL/Parity.thy
changeset 66582 2b49d4888cb8
parent 64785 ae0bbc8e45ad
child 66808 1907167b6038
     1.1 --- a/src/HOL/Parity.thy	Thu Aug 31 21:48:03 2017 +0200
     1.2 +++ b/src/HOL/Parity.thy	Sun Aug 27 06:27:01 2017 +0200
     1.3 @@ -242,6 +242,9 @@
     1.4  lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
     1.5    by simp
     1.6  
     1.7 +lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
     1.8 +  by (cases "even (n + k)") auto
     1.9 +
    1.10  end
    1.11  
    1.12  context linordered_idom