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.