【Coq】コンピューターで証明しよう【コック】©2ch.net

[0148 １３２人目の素数さん 2016/05/25(水) 20:46:14.27 ID:EofZeTbn]

まずはこれを解いてみるとか。

Require Import Omega.

Theorem t:
exists m : nat, 2^m > 1000.