ssrnat 練習

今度はソフトウェアの基礎の演習問題.

gist9c82a2ca96660cc64a87

cf. ソフトウェアの基礎

rewriteするときに, 右分配律mulSnrを使っています。 ------>> Ssreflect.ssrnatのMultiplication.にあるLemmaから.

牛刀振り回してる感じありますが、一応証明です。