The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Yakov Zaytsev wrote:
> I used omega to solve this inequality
>
>     Lemma zgtz : not (0 > 0).
>
> Now I can't get what does resulting term mean
>
>     Require Import Arith.
>     (*Require Import Omega.*)
>     Require Import Coq.ZArith.auxiliary. (* Zgt_left *)
>     Require Import Coq.ZArith.Znat. (* inj_gt *)
>     Parameter H: 0 > 0.
>     Definition left := Zgt_left 0 0 (inj_gt 0 0 H).
>     Definition zgtz := left (eq_refl Gt).
>
> Left doesn't have arrow type, does it!? Why is zgtz well-typed then?

In fact, [left] _does_ have a function type.  Its type is a call to 
[Zle], which evaluates to an expression built with [<>], which evaluates 
to the negation of an [=] fact.  A negation is encoded as a function 
returning [False] proofs.