new lemma
authornipkow
Mon Jun 08 09:58:41 2009 +0200 (2009-06-08)
changeset 315056f589131ba94
parent 31504 0566495a3986
child 31507 bd96f81f6572
new lemma
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Mon Jun 08 09:23:04 2009 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Jun 08 09:58:41 2009 +0200
     1.3 @@ -853,6 +853,12 @@
     1.4  apply (simp add: add_ac)
     1.5  done
     1.6  
     1.7 +lemma setsum_natinterval_difff:
     1.8 +  fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
     1.9 +  shows  "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
    1.10 +          (if m <= n then f m - f(n + 1) else 0)"
    1.11 +by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
    1.12 +
    1.13  
    1.14  subsection{* Shifting bounds *}
    1.15