src/HOL/SetInterval.thy
changeset 32408 a1a85b0a26f7
parent 32400 6c62363cf0d7
child 32436 10cd49e0c067
     1.1 --- a/src/HOL/SetInterval.thy	Wed Aug 26 10:48:45 2009 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Aug 26 16:13:19 2009 +0200
     1.3 @@ -242,6 +242,14 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma (in linorder) atLeastLessThan_subset_iff:
     1.8 +  "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
     1.9 +apply (auto simp:subset_eq Ball_def)
    1.10 +apply(frule_tac x=a in spec)
    1.11 +apply(erule_tac x=d in allE)
    1.12 +apply (simp add: less_imp_le)
    1.13 +done
    1.14 +
    1.15  subsection {* Intervals of natural numbers *}
    1.16  
    1.17  subsubsection {* The Constant @{term lessThan} *}