src/HOL/Set_Interval.thy

 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
 by blast
 
 subsubsection \<open>The Constant @{term greaterThan}\<close>
 
-lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
+lemma greaterThan_0: "greaterThan 0 = range Suc"
 apply (simp add: greaterThan_def)
 apply (blast dest: gr0_conv_Suc [THEN iffD1])
 done
 
 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"

 
 lemma sum_Suc_diff:
   fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
   assumes "m \<le> Suc n"
   shows "(\<Sum>i = m..n. f(Suc i) - f i) = f (Suc n) - f m"
+using assms by (induct n) (auto simp: le_Suc_eq)
+
+lemma sum_Suc_diff':
+  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+  assumes "m \<le> n"
+  shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
 using assms by (induct n) (auto simp: le_Suc_eq)
 
 lemma nested_sum_swap:
      "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
   by (induction n) (auto simp: sum.distrib)