src/HOL/Euclidean_Division.thy

--- a/src/HOL/Euclidean_Division.thy	Mon Mar 09 19:35:07 2020 +0100
+++ b/src/HOL/Euclidean_Division.thy	Sun Mar 08 17:07:49 2020 +0000
@@ -2002,6 +2002,10 @@
     by (simp add: of_nat_mod of_nat_diff)
 qed
 
+lemma of_bool_half_eq_0 [simp]:
+  \<open>of_bool b div 2 = 0\<close>
+  by simp
+
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat