get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays

Basically a new take on !677 (closed), but now based on stdpp!439 for Z-based list operations. That said, just changing the existing array lemmas to Z-based indexing would be a massive breaking change, so this keeps the old lemmas around as well.

To express the Z-based lemmas nicely, we need a version of big-star for lists that uses Z-based indexing. So, yet anothert big-op... :( . I ported the most basic lemmas for it, but there are still many big-sep lemmas that need to be ported (and many of these ports are non-trivial).

Fixes stdpp#102.