# HG changeset patch
# User nipkow
# Date 1503505736 -7200
# Node ID cc66ab2373ce87fe32b3a8610d8dff2fbaf06efc
# Parent  495df623251763a83d15e86c3c5d75c2513f07df
added lemma

diff -r 495df6232517 -r cc66ab2373ce 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)"