| changeset 79531 | 22a137a6de44 |
| parent 79118 | 486a32079c60 |
| child 79555 | 8ef205d9fd22 |
--- a/src/HOL/Parity.thy Thu Jan 25 17:08:07 2024 +0000 +++ b/src/HOL/Parity.thy Thu Jan 25 11:19:03 2024 +0000 @@ -925,7 +925,7 @@ context linordered_euclidean_semiring begin -lemma even_mask_div_iff': +lemma even_decr_exp_div_exp_iff': \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close> proof - have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close>