Rotate everything

This MR adds rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions, which allow dealing with wraparound of lists. I don't know where these functions should go so I created a new file for them. But I can also move them somewhere else.

Thanks for the MR.

Where to put this? We could put it in list, which is becoming a very long file, but I don't really mind. We cannot put it in numbers, since it needs stuff about lists, and numbers depends on list.

We could create a new file list_numbers or so, that also contains other operations on lists like seq and seqZ that involve numbers. We can then also move sum_list from numbers (which really should not be there!) to that file.

added 1 commit

• 0331f150 - Added list_numbers.v with rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions

Compare with previous version

I created a new list_numbers.v since my emacs does not like the large list.v file (probably due to company-coq) and moved the definitions you mentioned there. Should I move anything else? This is possibly a breaking change if one only imports list.v, but not prelude.v since the definitions where moved.

TODO: create to separate merge request for the moving with a CHANGELOG entry