diff -r f2c98b8c0c5c -r 2946b8f057df src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Jul 01 08:13:20 2010 +0200
+++ b/src/HOL/SetInterval.thy	Thu Jul 01 09:01:09 2010 +0200
@@ -456,6 +456,23 @@
   apply auto
   done
 
+lemma image_minus_const_atLeastLessThan_nat:
+  fixes c :: nat
+  shows "(\<lambda>i. i - c) ` {x ..< y} =
+      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
+    (is "_ = ?right")
+proof safe
+  fix a assume a: "a \<in> ?right"
+  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
+  proof cases
+    assume "c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ "a + c"])
+  next
+    assume "\<not> c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)
+  qed
+qed auto
+
 context ordered_ab_group_add
 begin