# HG changeset patch
# User haftmann
# Date 1244444580 -7200
# Node ID cca1281e63847275b560cc67605dd13396e49398
# Parent  2a60c9b951e0dd03c032d8c454c90fd7984930d9# Parent  e2de58666d21df421ad3e428274c65b4003c0fae
merged

diff -r e2de58666d21 -r cca1281e6384 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Jun 08 09:02:51 2009 +0200
+++ b/src/HOL/SetInterval.thy	Mon Jun 08 09:03:00 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}"