add mono_Z base-logic library

This has exactly the same lemmas as mono_nat. It is useful in cases where one wants to avoid nat entirely and use Z throughout.