| changeset 79017 | 127ba61b2630 |
| parent 78935 | 5e788ff7a489 |
| child 80061 | 4c1347e172b1 |
--- 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]: