証明を書くのが大変だというけど、プログラムを書く以上に
大変なわけではないよ。証明はプログラムでもあるわけだから。