順序対の定義。 結構きつかったのでコメントもなしにガリガリ書いていた。もっときれいなやり方があるはず。 順序対の定義と性質 相変わらず、ComprehensionとかReplacementは先送りにしていますがどうなることか。

コメントなしコードだけ。 0 /= { 0 } の証明が一応出来ました。 ZFCカッコ仮

今度はソフトウェアの基礎の演習問題. gist9c82a2ca96660cc64a87 cf. ソフトウェアの基礎 rewriteするときに, 右分配律mulSnrを使っています。 ------>> Ssreflect.ssrnatのMultiplication.にあるLemmaから. 牛刀振り回してる感じありますが、一応証明です。

ssrboolの練習。とりあえずソフトウェアの基礎とか見ながらやってます。 ssreflectっぽくないですが、そのうちrewriteとかガリガリ使っていきたいです。 gist31a74ec01b8961c4f506