src/HOL/Set_Interval.thy

--- a/src/HOL/Set_Interval.thy	Wed Aug 23 14:37:22 2017 +0200
+++ b/src/HOL/Set_Interval.thy	Wed Aug 23 18:28:56 2017 +0200
@@ -1894,6 +1894,9 @@
 
 subsection \<open>The formula for geometric sums\<close>
 
+lemma sum_power2: "(\<Sum>i=0..<k. (2::nat)^i) = 2^k-1"
+by (induction k) (auto simp: mult_2)
+
 lemma geometric_sum:
   assumes "x \<noteq> 1"
   shows "(\<Sum>i<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"