src/HOL/Set_Interval.thy

 breaks many proofs. Since it only helps blast, it is better to leave them
 alone.\<close>
 
 lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
   by auto
+
+lemma (in order) atLeast_lessThan_eq_atLeast_atMost_diff:
+  "{a..<b} = {a..b} - {b}"
+  by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
 
 end
 
 subsubsection\<open>Emptyness, singletons, subset\<close>
 

 lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
   apply (induct k)
   apply (simp_all add: atLeastLessThanSuc)
   done
 
+
 subsubsection \<open>Intervals and numerals\<close>
 
 lemma lessThan_nat_numeral:  \<comment>\<open>Evaluation for specific numerals\<close>
   "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))"
   by (simp add: numeral_eq_Suc lessThan_Suc)

   "atLeastLessThan m (numeral k :: nat) =
      (if m \<le> (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k))
                  else {})"
   by (simp add: numeral_eq_Suc atLeastLessThanSuc)
 
+
 subsubsection \<open>Image\<close>
 
-lemma image_add_atLeastAtMost [simp]:
-  fixes k ::"'a::linordered_semidom"
-  shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
+context linordered_semidom
+begin
+
+lemma image_add_atLeast_atMost [simp]:
+  "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
 proof
-  show "?A \<subseteq> ?B" by auto
+  show "?A \<subseteq> ?B"
+    by (auto simp add: ac_simps)
 next
   show "?B \<subseteq> ?A"
   proof
-    fix n assume a: "n : ?B"
-    hence "n - k : {i..j}"
+    fix n
+    assume "n \<in> ?B"
+    then have "i \<le> n - k"
+      by (simp add: add_le_imp_le_diff)
+    have "n = n - k + k"
+    proof -
+      from \<open>n \<in> ?B\<close> have "n = n - (i + k) + (i + k)"
+        by simp
+      also have "\<dots> = n - k - i + i + k"
+        by (simp add: algebra_simps)
+      also have "\<dots> = n - k + k"
+        using \<open>i \<le> n - k\<close> by simp
+      finally show ?thesis .
+    qed
+    moreover have "n - k \<in> {i..j}"
+      using \<open>n \<in> ?B\<close>
       by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)
-    moreover have "n = (n - k) + k" using a
-    proof -
-      have "k + i \<le> n"
-        by (metis a add.commute atLeastAtMost_iff)
-      hence "k + (n - k) = n"
-        by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse)
-      thus ?thesis
-        by (simp add: add.commute)
-    qed
-    ultimately show "n : ?A" by blast
+    ultimately show "n \<in> ?A"
+      by (simp add: ac_simps) 
   qed
 qed
 
+lemma image_add_atLeast_atMost' [simp]:
+  "(\<lambda>n. n + k) ` {i..j} = {i + k..j + k}"
+  by (simp add: add.commute [of _ k])
+
+lemma image_add_atLeast_lessThan [simp]:
+  "plus k ` {i..<j} = {i + k..<j + k}"
+  by (simp add: image_set_diff atLeast_lessThan_eq_atLeast_atMost_diff ac_simps)
+
+lemma image_add_atLeast_lessThan' [simp]:
+  "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
+  by (simp add: add.commute [of _ k])
+
+end
+
+lemma image_Suc_atLeast_atMost [simp]:
+  "Suc ` {i..j} = {Suc i..Suc j}"
+  using image_add_atLeast_atMost [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+lemma image_Suc_atLeast_lessThan [simp]:
+  "Suc ` {i..<j} = {Suc i..<Suc j}"
+  using image_add_atLeast_lessThan [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+corollary image_Suc_atMost:
+  "Suc ` {..n} = {1..Suc n}"
+  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+corollary image_Suc_lessThan:
+  "Suc ` {..<n} = {1..n}"
+  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+  
 lemma image_diff_atLeastAtMost [simp]:
   fixes d::"'a::linordered_idom" shows "(op - d ` {a..b}) = {d-b..d-a}"
   apply auto
   apply (rule_tac x="d-x" in rev_image_eqI, auto)
   done

   shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
             else if 0 \<le> m then {a/m - c .. b/m - c}
             else {b/m - c .. a/m - c})"
   using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
   by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma image_add_atLeastLessThan:
-  "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B")
-proof
-  show "?A \<subseteq> ?B" by auto
-next
-  show "?B \<subseteq> ?A"
-  proof
-    fix n assume a: "n : ?B"
-    hence "n - k : {i..<j}" by auto
-    moreover have "n = (n - k) + k" using a by auto
-    ultimately show "n : ?A" by blast
-  qed
-qed
-
-corollary image_Suc_lessThan:
-  "Suc ` {..<n} = {1..n}"
-  using image_add_atLeastLessThan [of 1 0 n]
-  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
-
-corollary image_Suc_atMost:
-  "Suc ` {..n} = {1..Suc n}"
-  using image_add_atLeastLessThan [of 1 0 "Suc n"]
-  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
-
-corollary image_Suc_atLeastAtMost[simp]:
-  "Suc ` {i..j} = {Suc i..Suc j}"
-using image_add_atLeastAtMost[where k="Suc 0"] by simp
-
-corollary image_Suc_atLeastLessThan[simp]:
-  "Suc ` {i..<j} = {Suc i..<Suc j}"
-using image_add_atLeastLessThan[where k="Suc 0"] by simp
 
 lemma atLeast1_lessThan_eq_remove0:
   "{Suc 0..<n} = {..<n} - {0}"
   by auto
 

     assume "\<not> c < y" with a show ?thesis
       by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
   qed
 qed auto
 
-lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
+lemma image_int_atLeast_lessThan:
+  "int ` {a..<b} = {int a..<int b}"
+  by (auto intro!: image_eqI [where x = "nat x" for x])
+
+lemma image_int_atLeast_atMost:
+  "int ` {a..b} = {int a..int b}"
   by (auto intro!: image_eqI [where x = "nat x" for x])
 
 context ordered_ab_group_add
 begin
 

 done
 
 
 subsection \<open>Generic big monoid operation over intervals\<close>
 
-lemma inj_on_add_nat' [simp]:
-  "inj_on (plus k) N" for k :: nat
+context semiring_char_0
+begin
+
+lemma inj_on_of_nat [simp]:
+  "inj_on of_nat N"
   by rule simp
+
+lemma bij_betw_of_nat [simp]:
+  "bij_betw of_nat N A \<longleftrightarrow> of_nat ` N = A"
+  by (simp add: bij_betw_def)
+
+end
 
 context comm_monoid_set
 begin
 
+lemma atLeast_lessThan_reindex:
+  "F g {h m..<h n} = F (g \<circ> h) {m..<n}"
+  if "bij_betw h {m..<n} {h m..<h n}" for m n ::nat
+proof -
+  from that have "inj_on h {m..<n}" and "h ` {m..<n} = {h m..<h n}"
+    by (simp_all add: bij_betw_def)
+  then show ?thesis
+    using reindex [of h "{m..<n}" g] by simp
+qed
+
+lemma atLeast_atMost_reindex:
+  "F g {h m..h n} = F (g \<circ> h) {m..n}"
+  if "bij_betw h {m..n} {h m..h n}" for m n ::nat
+proof -
+  from that have "inj_on h {m..n}" and "h ` {m..n} = {h m..h n}"
+    by (simp_all add: bij_betw_def)
+  then show ?thesis
+    using reindex [of h "{m..n}" g] by simp
+qed
+
 lemma atLeast_lessThan_shift_bounds:
-  fixes m n k :: nat
-  shows "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
-proof -
-  have "{m + k..<n + k} = plus k ` {m..<n}"
-    by (auto simp add: image_add_atLeastLessThan [symmetric])
-  also have "F g (plus k ` {m..<n}) = F (g \<circ> plus k) {m..<n}"
-    by (rule reindex) simp
-  finally show ?thesis .
-qed
+  "F g {m + k..<n + k} = F (g \<circ> plus k) {m..<n}"
+  for m n k :: nat
+  using atLeast_lessThan_reindex [of "plus k" m n g]
+  by (simp add: ac_simps)
 
 lemma atLeast_atMost_shift_bounds:
-  fixes m n k :: nat
-  shows "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
-proof -
-  have "{m + k..n + k} = plus k ` {m..n}"
-    by (auto simp del: image_add_atLeastAtMost simp add: image_add_atLeastAtMost [symmetric])
-  also have "F g (plus k ` {m..n}) = F (g \<circ> plus k) {m..n}"
-    by (rule reindex) simp
-  finally show ?thesis .
-qed
+  "F g {m + k..n + k} = F (g \<circ> plus k) {m..n}"
+  for m n k :: nat
+  using atLeast_atMost_reindex [of "plus k" m n g]
+  by (simp add: ac_simps)
 
 lemma atLeast_Suc_lessThan_Suc_shift:
   "F g {Suc m..<Suc n} = F (g \<circ> Suc) {m..<n}"
-  using atLeast_lessThan_shift_bounds [of _ _ 1] by simp
+  using atLeast_lessThan_shift_bounds [of _ _ 1]
+  by (simp add: plus_1_eq_Suc)
 
 lemma atLeast_Suc_atMost_Suc_shift:
   "F g {Suc m..Suc n} = F (g \<circ> Suc) {m..n}"
-  using atLeast_atMost_shift_bounds [of _ _ 1] by simp
+  using atLeast_atMost_shift_bounds [of _ _ 1]
+  by (simp add: plus_1_eq_Suc)
+
+lemma atLeast_int_lessThan_int_shift:
+  "F g {int m..<int n} = F (g \<circ> int) {m..<n}"
+  by (rule atLeast_lessThan_reindex)
+    (simp add: image_int_atLeast_lessThan)
+
+lemma atLeast_int_atMost_int_shift:
+  "F g {int m..int n} = F (g \<circ> int) {m..n}"
+  by (rule atLeast_atMost_reindex)
+    (simp add: image_int_atLeast_atMost)
 
 lemma atLeast0_lessThan_Suc:
   "F g {0..<Suc n} = F g {0..<n} \<^bold>* g n"
   by (simp add: atLeast0_lessThan_Suc ac_simps)
 

 by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
 
 lemma nat_diff_sum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
   by (rule sum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
 
+lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x  \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
+  by (subst sum_subtractf_nat) auto
+
 
 subsubsection \<open>Shifting bounds\<close>
 
 lemma sum_shift_bounds_nat_ivl:
   "sum f {m+k..<n+k} = sum (%i. f(i + k)){m..<n::nat}"

 
 corollary sum_shift_bounds_Suc_ivl:
   "sum f {Suc m..<Suc n} = sum (%i. f(Suc i)){m..<n}"
 by (simp add:sum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
 
+context comm_monoid_add
+begin
+
+context
+  fixes f :: "nat \<Rightarrow> 'a"
+  assumes "f 0 = 0"
+begin
+
+lemma sum_shift_lb_Suc0_0_upt:
+  "sum f {Suc 0..<k} = sum f {0..<k}"
+proof (cases k)
+  case 0
+  then show ?thesis
+    by simp
+next
+  case (Suc k)
+  moreover have "{0..<Suc k} = insert 0 {Suc 0..<Suc k}"
+    by auto
+  ultimately show ?thesis
+    using \<open>f 0 = 0\<close> by simp
+qed
+
 lemma sum_shift_lb_Suc0_0:
-  "f(0::nat) = (0::nat) \<Longrightarrow> sum f {Suc 0..k} = sum f {0..k}"
-by(simp add:sum_head_Suc)
-
-lemma sum_shift_lb_Suc0_0_upt:
-  "f(0::nat) = 0 \<Longrightarrow> sum f {Suc 0..<k} = sum f {0..<k}"
-apply(cases k)apply simp
-apply(simp add:sum_head_upt_Suc)
-done
+  "sum f {Suc 0..k} = sum f {0..k}"
+proof (cases k)
+  case 0
+  with \<open>f 0 = 0\<close> show ?thesis
+    by simp
+next
+  case (Suc k)
+  moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}"
+    by auto
+  ultimately show ?thesis
+    using \<open>f 0 = 0\<close> by simp
+qed
+
+end
+
+end
 
 lemma sum_atMost_Suc_shift:
   fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
   shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
 proof (induct n)

 lemma sum_lessThan_telescope':
   "(\<Sum>n<m. f n - f (Suc n) :: 'a :: ab_group_add) = f 0 - f m"
   by (induction m) (simp_all add: algebra_simps)
 
 
-subsection \<open>The formula for geometric sums\<close>
+subsubsection \<open>The formula for geometric sums\<close>
 
 lemma sum_power2: "(\<Sum>i=0..<k. (2::nat)^i) = 2^k-1"
 by (induction k) (auto simp: mult_2)
 
 lemma geometric_sum:

                 else if x = 1 then of_nat((n + 1) - m)
                 else (x^m - x^Suc n) / (1 - x))"
 using sum_gp_multiplied [of m n x] apply auto
 by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
 
-subsection\<open>Geometric progressions\<close>
+
+subsubsection\<open>Geometric progressions\<close>
 
 lemma sum_gp0:
   fixes x :: "'a::{comm_ring,division_ring}"
   shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
   using sum_gp_basic[of x n]

 lemma sum_gp_strict:
   fixes x :: "'a::{comm_ring,division_ring}"
   shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
   by (induct n) (auto simp: algebra_simps divide_simps)
 
-subsubsection \<open>The formula for arithmetic sums\<close>
+
+subsubsection \<open>The formulae for arithmetic sums\<close>
+
+context comm_semiring_1
+begin
+
+lemma double_gauss_sum:
+  "2 * (\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)"
+  by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice)
+
+lemma double_gauss_sum_from_Suc_0:
+  "2 * (\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)"
+proof -
+  have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})"
+    by simp
+  also have "\<dots> = sum of_nat {0..n}"
+    by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0)
+  finally show ?thesis
+    by (simp add: double_gauss_sum)
+qed
+
+lemma double_arith_series:
+  "2 * (\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)"
+proof -
+  have "(\<Sum>i = 0..n. a + of_nat i * d) = ((\<Sum>i = 0..n. a) + (\<Sum>i = 0..n. of_nat i * d))"
+    by (rule sum.distrib)
+  also have "\<dots> = (of_nat (Suc n) * a + d * (\<Sum>i = 0..n. of_nat i))"
+    by (simp add: sum_distrib_left algebra_simps)
+  finally show ?thesis
+    by (simp add: algebra_simps double_gauss_sum left_add_twice)
+qed
+
+end
+
+context semiring_parity
+begin
 
 lemma gauss_sum:
-  "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) = of_nat n*((of_nat n)+1)"
-proof (induct n)
+  "(\<Sum>i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"
+  using double_gauss_sum [of n, symmetric] by simp
+
+lemma gauss_sum_from_Suc_0:
+  "(\<Sum>i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2"
+  using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp
+
+lemma arith_series:
+  "(\<Sum>i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2"
+  using double_arith_series [of a d n, symmetric] by simp
+
+end
+
+lemma gauss_sum_nat:
+  "\<Sum>{0..n} = (n * Suc n) div 2"
+  using gauss_sum [of n, where ?'a = nat] by simp
+
+lemma arith_series_nat:
+  "(\<Sum>i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2"
+  using arith_series [of a d n] by simp
+
+lemma Sum_Icc_int:
+  "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2"
+  if "m \<le> n" for m n :: int
+using that proof (induct i \<equiv> "nat (n - m)" arbitrary: m n)
   case 0
-  show ?case by simp
+  then have "m = n"
+    by arith
+  then show ?case
+    by (simp add: algebra_simps mult_2 [symmetric])
 next
-  case (Suc n)
-  then show ?case
-    by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)
-      (* FIXME: make numeral cancellation simprocs work for semirings *)
-qed
-
-theorem arith_series_general:
-  "(2::'a::comm_semiring_1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
-  of_nat n * (a + (a + of_nat(n - 1)*d))"
-proof cases
-  assume ngt1: "n > 1"
-  let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
-  have
-    "(\<Sum>i\<in>{..<n}. a+?I i*d) =
-     ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
-    by (rule sum.distrib)
-  also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
-  also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
-    unfolding One_nat_def
-    by (simp add: sum_distrib_left atLeast0LessThan[symmetric] sum_shift_lb_Suc0_0_upt ac_simps)
-  also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
-    by (simp add: algebra_simps)
-  also from ngt1 have "{1..<n} = {1..n - 1}"
-    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
-  also from ngt1
-  have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
-    by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)
-      (simp add:  mult.commute trans [OF add.commute of_nat_Suc [symmetric]])
+  case (Suc i)
+  have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
+  have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
+  also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
+    by(subst atLeastAtMostPlus1_int_conv) simp_all
+  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
+    by(simp add: Suc(1)[OF 0])
+  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
+  also have "\<dots> = (n*(n+1) - m*(m-1)) div 2"
+    by (simp add: algebra_simps mult_2_right)
+  finally show ?case .
+qed
+
+lemma Sum_Icc_nat:
+  "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2"
+  if "m \<le> n" for m n :: nat
+proof -
+  have *: "m * (m - 1) \<le> n * (n + 1)"
+    using that by (meson diff_le_self order_trans le_add1 mult_le_mono)
+  have "int (\<Sum>{m..n}) = (\<Sum>{int m..int n})"
+    by (simp add: sum.atLeast_int_atMost_int_shift)
+  also have "\<dots> = (int n * (int n + 1) - int m * (int m - 1)) div 2"
+    using that by (simp add: Sum_Icc_int)
+  also have "\<dots> = int ((n * (n + 1) - m * (m - 1)) div 2)"
+    using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff)
   finally show ?thesis
-    unfolding mult_2 by (simp add: algebra_simps)
-next
-  assume "\<not>(n > 1)"
-  hence "n = 1 \<or> n = 0" by auto
-  thus ?thesis by (auto simp: mult_2)
-qed
-
-lemma arith_series_nat:
-  "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
+    by (simp only: of_nat_eq_iff)
+qed
+
+lemma Sum_Ico_nat: 
+  "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2"
+  if "m \<le> n" for m n :: nat
 proof -
-  have
-    "2 * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
-    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
-    by (rule arith_series_general)
-  thus ?thesis
-    unfolding One_nat_def by auto
-qed
-
-lemma arith_series_int:
-  "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
-  by (fact arith_series_general) (* FIXME: duplicate *)
-
-lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x  \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
-  by (subst sum_subtractf_nat) auto
+  from that consider "m < n" | "m = n"
+    by (auto simp add: less_le)
+  then show ?thesis proof cases
+    case 1
+    then have "{m..<n} = {m..n - 1}"
+      by auto
+    then have "\<Sum>{m..<n} = \<Sum>{m..n - 1}"
+      by simp
+    also have "\<dots> = (n * (n - 1) - m * (m - 1)) div 2"
+      using \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute)
+    finally show ?thesis .
+  next
+    case 2
+    then show ?thesis
+      by simp
+  qed
+qed
 
 
 subsubsection \<open>Division remainder\<close>
 
 lemma range_mod: