二進表現じゃない整数型

この前作ったマイポジティブ型は、ペアノの公理を元にした形式化だったので、それを使って、ペアノゼットという整数型を作ってみた。
既存のポジティブ型とマイポジティブ型との間の同型対応は、前回示してあるので、それをもとにしている既存のZ型とペアノゼット型との間の同型も示すことができる（ここでいう同型とは、環同型および順序同型のことである）。
よって、新たに作ったPeanoZという整数型に対しても、既存のZとその演算に関する全ての定理が成り立つことが示せる。さらに、今後ZもしくはPeanoZで示すことができた性質は、両方で成り立つことが保証されるのである。