Coqで証明をする動画を作って、にこにこ動画に公開した。 http://www.nicovideo.jp/watch/sm1276083

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

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

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