16.2 Using Omega
The tactic Omega does not belong to the core system. It should be
loaded by
Coq < Require Omega.
Example 6:
Coq < Goal (m,n:Z) ~ `1+2*m = 2*n`.
1 subgoal
============================
(m,n:Z)`1+2*m <> 2*n`
Coq < Intros; Omega.
Subtree proved!
Example 7:
Coq < Goal (z:Z)`z>0` -> `2*z + 1 > z`.
1 subgoal
============================
(z:Z)`z > 0`->`2*z+1 > z`
Coq < Intro; Omega.
Subtree proved!
Other examples can be found in $COQLIB/theories/DEMOS/OMEGA
.