離散数学の授業で定理証明器のことをちょっと触れたいと思って、証明の例題に使っている上記命題をCoqで証明してみました。多分いろいろ上手くないと思うのだけれどもさらしてみます。 Require Import Classical. Require Import Arith. Require Import Omeg…