次に、このPeanoPositiveを使って、PeanoZという整数型を作った。

まずこの前のコードに引き算のレンマを加えて、PeanoPositive.vとしてまとめた。

この前作ったマイポジティブ型は、ペアノの公理を元にした形式化だったので、それを使って、ペアノゼットという整数型を作ってみた。 既存のポジティブ型とマイポジティブ型との間の同型対応は、前回示してあるので、それをもとにしている既存のZ型とペアノ…