1.1 --- a/src/HOL/Set_Interval.thy	Fri Feb 15 09:59:46 2013 +0100
     1.2 +++ b/src/HOL/Set_Interval.thy	Fri Feb 15 10:52:47 2013 +0100
     1.3 @@ -564,6 +564,9 @@
     1.4    qed
     1.5  qed auto
     1.6  
     1.7 +lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
     1.8 +by(auto intro!: image_eqI[where x="nat x", standard])
     1.9 +
    1.10  context ordered_ab_group_add
    1.11  begin
    1.12