diff -r 5f179549c362 -r 2f65dcd32a59 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Nov 11 14:46:26 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Tue Nov 11 19:38:45 2014 +0100
@@ -488,6 +488,19 @@
 lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
   by (simp add: Iio_eq_empty_iff bot_nat_def)
 
+lemma mono_image_least:
+  assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n"
+  shows "f m = m'"
+proof -
+  from f_img have "{m' ..< n'} \<noteq> {}"
+    by (metis atLeastLessThan_empty_iff image_is_empty)
+  with f_img have "m' \<in> f ` {m ..< n}" by auto
+  then obtain k where "f k = m'" "m \<le> k" by auto
+  moreover have "m' \<le> f m" using f_img by auto
+  ultimately show "f m = m'"
+    using f_mono by (auto elim: monoE[where x=m and y=k])
+qed
+
 
 subsection {* Infinite intervals *}