Coq introduction reference http://www.iij-ii.co.jp/lab/techdoc/coqt/ http://www.ne.jp/asahi/fmsci/fmmath/coqp/acindex.html http://study-func-prog.blogspot.jp/2012/04/coq-group-on-setoid.html http://ccvanishing.hateblo.jp/?page=1358683043 http://qnighy.github.io/coqex2014/ex2.html