diff -r 74440d820ba5 -r 127ba61b2630 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue Nov 21 19:19:16 2023 +0000
+++ b/src/HOL/Groups_List.thy	Tue Nov 21 19:19:16 2023 +0000
@@ -447,6 +447,10 @@
     by (simp add: * algebra_simps)
 qed
 
+lemma horner_sum_of_bool_2_less:
+  \<open>(horner_sum of_bool 2 bs) < 2 ^ length bs\<close>
+  by (fact horner_sum_bound)
+
 end
 
 lemma nat_horner_sum [simp]: