new lemma

--- 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 *}