I think the Open Scope Z_scope in heap_lang.lang is a mistake. While Zs are often useful when working with HeapLang, I don't think HeapLang should enforce that on users. Furthermore, whether one actually gets an opened Z_scope or not seems to depend on the import order (see this discussion on Mattermost).
In this MR I thus remove Open Scope Z_scope. According to grep, after this MR, there are no other scopes that are opened globally (apart from general_if_scope in algebra.base which is to patch up ssreflect).
As a consequence of this change, some %Z had to be inserted, while it also allowed for some %nats to be removed.