# HG changeset patch
# User Andreas Lochbihler
# Date 1360921967 -3600
# Node ID b52cc015429a78a34024550ce8ace7ebae4e97ad
# Parent  59e311235de4cbaf2845997da5db86f05ccbe279
added lemma

diff -r 59e311235de4 -r b52cc015429a src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Feb 15 09:59:46 2013 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Feb 15 10:52:47 2013 +0100
@@ -564,6 +564,9 @@
   qed
 qed auto
 
+lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
+by(auto intro!: image_eqI[where x="nat x", standard])
+
 context ordered_ab_group_add
 begin