The Coq mailing list

[Yakov Zaytsev <yakov AT yakov.cc>]

Hello,

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?

-- Yakov