Ranges of naturals as lists #
This file shows basic results about
finRange n is the list of elements of
iota n = [n, n - 1, ..., 1] and
range n = [0, ..., n - 1] are basic list constructions used for
range' a b = [a, ..., a + b - 1] is there to help prove properties about them.
Actual maths should use