Extra lemmas about intervals
This file contains lemmas about intervals that cannot be included into
because this would create an
import cycle. Namely, lemmas in this file can use definitions
If two half-open intervals are disjoint and the endpoint of one lies in the other, then it must be equal to the endpoint of the other.