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