17.2 Using Omega

17.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 ca be found in $COQLIB/theories/DEMOS/OMEGA.

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.6.1.html at 8/10/98