# HG changeset patch
# User nipkow
# Date 1244447921 -7200
# Node ID 6f589131ba94f8f86a3f9716ecf09f88c2d77d60
# Parent  0566495a3986afa565b7566d9612857ad89b14e8
new lemma

diff -r 0566495a3986 -r 6f589131ba94 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Jun 08 09:23:04 2009 +0200
+++ b/src/HOL/SetInterval.thy	Mon Jun 08 09:58:41 2009 +0200
@@ -853,6 +853,12 @@
 apply (simp add: add_ac)
 done
 
+lemma setsum_natinterval_difff:
+  fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
+  shows  "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
+          (if m <= n then f m - f(n + 1) else 0)"
+by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
+
 
 subsection{* Shifting bounds *}