--- a/src/HOL/Divides.thy Sat Jul 11 18:19:08 2020 +0200
+++ b/src/HOL/Divides.thy Sat Jul 11 18:09:08 2020 +0000
@@ -753,6 +753,32 @@
thus ?lhs by simp
qed
+lemma take_bit_greater_eq:
+ \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
+proof -
+ have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
+ proof (cases \<open>k > - (2 ^ n)\<close>)
+ case False
+ then have \<open>k + 2 ^ n \<le> 0\<close>
+ by simp
+ also note take_bit_nonnegative
+ finally show ?thesis .
+ next
+ case True
+ with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
+ by simp_all
+ then show ?thesis
+ by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
+ qed
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_less_eq:
+ \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
+ using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
+ by (simp add: take_bit_eq_mod)
+
subsection \<open>Numeral division with a pragmatic type class\<close>