Ico n m is the list of natural numbers
n ≤ x < m.
(Ico stands for "interval, closed-open".)
@TODO (anyone): Define
Icc, state basic lemmas about them.
@TODO (anyone): Prove that
@TODO (anyone): Also do the versions for integers?
@TODO (anyone): One could generalise even further, defining
'locally finite partial orders', for which
set.Ico a b is
'locally finite total orders', for which there is a list model.