All elements of fin n, from 0 to n-1.
A variant of prod_range_succ which pulls off the first
term in the product rather than the last.
A variant of sum_range_succ which pulls off the first term in the sum
rather than the last.