src/HOL/Set_Interval.thy

--- a/src/HOL/Set_Interval.thy	Tue May 17 08:40:24 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Tue May 17 17:05:35 2016 +0200
@@ -1640,6 +1640,10 @@
   finally show ?case .
 qed
 
+lemma setsum_lessThan_Suc_shift:
+  "(\<Sum>i<Suc n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
+  by (induction n) (simp_all add: add_ac)
+
 lemma setsum_atMost_shift:
   fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
   shows "(\<Sum>i\<le>n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"