changeset 31505 | 6f589131ba94 |
parent 31501 | 2a60c9b951e0 |
child 31509 | 00ede188c5d6 |
--- 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 *}