src/HOL/Parity.thy
changeset 68157 057d5b4ce47e
parent 68028 1f9f973eed2a
child 68390 1c84a8c513af
     1.1 --- a/src/HOL/Parity.thy	Sat May 12 17:53:12 2018 +0200
     1.2 +++ b/src/HOL/Parity.thy	Sat May 12 22:20:46 2018 +0200
     1.3 @@ -542,6 +542,10 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma not_mod2_eq_Suc_0_eq_0 [simp]:
     1.8 +  "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
     1.9 +  using not_mod_2_eq_1_eq_0 [of n] by simp
    1.10 +
    1.11  
    1.12  subsection \<open>Parity and powers\<close>
    1.13