[Coq] Puzzle from Hiyama-san's Blog

　檜山さんのblogに掛け算から足し算を作る（パズルとしてやってみよう）という問題が載っています。
　Coqの練習問題としてちょうど良いかと思い解いてみました。
　思ったより時間がかかってしまい、解き終わる前にネタばらしが出ちゃったのだけど、一応、解いた解答です。http://ideone.com/Staa3

　分配則は簡単だったが、交換則を思いつくまでに苦労した。交換測を思いついたらその延長で結合則もなんとか。ただ、証明はちまちまとrewriteしてるだけ。ここは本当は自動化できるんだろうなぁ。
　Coq初心者的には、inv関係の{a'|a*a'=1}みたいな記法の使い方に慣れたのが良かったか。あとAxiom eq_dec_0:forall a:G, {a=0}+{a<>0}みたいなdecide出来る公理の便利さを実感した。