# HG changeset patch
# User nipkow
# Date 1244443938 -7200
# Node ID 2a60c9b951e0dd03c032d8c454c90fd7984930d9
# Parent  eced346b2231081e544236f15ed8a4f00f003cde
New lemma

diff -r eced346b2231 -r 2a60c9b951e0 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Jun 08 00:26:57 2009 +0200
+++ b/src/HOL/SetInterval.thy	Mon Jun 08 08:52:18 2009 +0200
@@ -833,6 +833,13 @@
 apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
 done
 
+lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1"
+  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
+proof-
+  have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using `m \<le> n+1` by auto
+  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint
+    atLeastSucAtMost_greaterThanAtMost)
+qed
 
 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"