Add `max_Z`/`mono_Z` camera

This MR provides the max_Z and mono_Z cameras.

---

Old This is an alternative to !880 (merged):

• Pro of this MR: It also provides algebra instances max_Z and mono_Z
• Pro of this MR: You can use mono_Z with negative integers. For example, you could use it to verify a counter that has an initial value that is negative.
• Con of this MR: You do not have the rule ⊢ |==> mono_Z_lb_own γ 0 since the actual value could be negative.