Extra lemmas about intervals
This file contains lemmas about intervals that cannot be included into data.set.intervals.basic
because this would create an import cycle. Namely, lemmas in this file can use definitions
from data.set.lattice, including disjoint.
@[simp]
@[simp]
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.