Add `Z`-based list operations

This came up here: it would be very useful to be able to interact with lists through an entirely Z-based interface -- in particular for length and lookup. take and drop have also been mentioned.

For some of these operations, questions remain about the desired behavior on negative inputs. Currently, l !! Z.to_nat z is common, but that will mean negative inputs return the list head --I think returning None probably makes more sense.

Another concern is lia integration.