さあ！証明しよう！

今日紹介するコマンドはProofコマンドだ。
このコマンドは何もしない。
Proofというからには、自動証明をやってくれるだろう、とか、何かすごいCoqの力で証明が変形するのかな、とか思う人がいるかもしれないが、このコマンドは何もしない。
このコマンドをいつでも、何回でも使うことができるが、使わなくても結果はかわらない。「これから証明するぞ！」という意気込みを表す勢いだけのコマンドである。
しかしあなどってはならない。このコマンドを証明の最初に入力することによって、どんな難問でも証明できてしまうような勇気がでてくるのだ。このことは紙での証明でも同じで、非常に重要であるように感じる。なぜなら証明するために必要な要素は勇気だからである。
Coqの取り扱い説明書にも、証明の最初にProofコマンドを使う奴は男前だと書いてある！
今日から証明するときにはプルーフ！と堂々と宣言しよう！