diff -r 3253aaf73a01 -r fcf90317383d src/HOL/Set_Interval.thy
--- 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 *}