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

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