The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Thanks Daniel and Jason.

> It seems highly unlikely, assuming your Z.le is like Zle from Coq
> 8.3pl4 and reduces to "fun x y => ((x ?= y) = Gt -> False)".

It is indeed the definition I am using.

> Or at least, without using some form of functional extensionality.

I need functional extensionality for other parts of this development,
so I will probably go that way.

> On the other hand, if Zle (and presumably Ple) were defined as
> inductive propositions, it would probably be possible.  By that, I'm
> thinking of something like (read this as pseudo-code):

Actually, I think that Z.le could be defined as
Definition Zle n m := n ?=m = Lt  \/ n ?= m = Eq.

This definition is compatible with proof irrelevance, and should be
completely equivalent with the previous one. I may try to submit a
feature request about that one, but I wonder if it is worth it.

Thomas