| changeset 68157 | 057d5b4ce47e |
| parent 68028 | 1f9f973eed2a |
| child 68389 | 1c84a8c513af |
--- a/src/HOL/Parity.thy Sat May 12 17:53:12 2018 +0200 +++ b/src/HOL/Parity.thy Sat May 12 22:20:46 2018 +0200 @@ -542,6 +542,10 @@ qed qed +lemma not_mod2_eq_Suc_0_eq_0 [simp]: + "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0" + using not_mod_2_eq_1_eq_0 [of n] by simp + subsection \<open>Parity and powers\<close>