The Coq mailing list

["Yevgeniy Makarov" <emakarov AT gmail.com>]

This is correct. You cannot match on (x < y). You may write

match (nat_compare x y) with
| Lt => ...
| Gt => ...
| Eq => ...
end.

There is also a boolean analog of <=:  leb : nat -> nat -> bool (these
functions are in Coq.Arith.Compare_dec).

You can also match on the /proofs/ of x < y. For example, you may prove

Lemma lt_sum : forall x y : nat, x < y -> exists z, x + z = y.
Proof.
intros x y H; induction H. ...

and then if you say

compute delta [lt_sum le_ind] in x.

then you'll see a match on an object of type x < y. However, in
applying match to proofs one may return only other proofs. For
example, you cannot return a number 1 if x < y has been proved using
the constructor le_n and 2 if it has been proved using le_S.

Evgeny