| changeset 60762 | bf0c76ccee8d |
| parent 60758 | d8d85a8172b5 |
| child 60809 | 457abb82fb9e |
--- a/src/HOL/Set_Interval.thy Mon Jul 20 11:40:43 2015 +0200 +++ b/src/HOL/Set_Interval.thy Mon Jul 20 23:12:50 2015 +0100 @@ -1357,6 +1357,10 @@ "{..< n} - {..< m} = {m ..< n}" by auto +lemma (in linorder) atLeastAtMost_diff_ends: + "{a..b} - {a, b} = {a<..<b}" + by auto + subsubsection \<open>Some Subset Conditions\<close>