Pretty-print 0 as "0" for N, Z, and nat
Alternative to #198 that is correct. This MR also:
- Adds test cases.
- Proves injectivity of
prettyforZ. - Refactored the code a bit by turning some results into lemmas.
Alternative to #198 that is correct. This MR also:
pretty for Z.