--- a/src/HOL/Set_Interval.thy Tue Mar 18 22:11:46 2014 +0100
+++ b/src/HOL/Set_Interval.thy Wed Mar 19 14:54:45 2014 +0000
@@ -1476,6 +1476,16 @@
"(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
by (induction n) (auto simp: setsum_addf)
+lemma nested_setsum_swap':
+ "(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
+ by (induction n) (auto simp: setsum_addf)
+
+lemma setsum_zero_power [simp]:
+ fixes c :: "nat \<Rightarrow> 'a::division_ring"
+ shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
+apply (cases "finite A")
+ by (induction A rule: finite_induct) auto
+
subsection {* The formula for geometric sums *}