The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 22/11/2016 10:36, noam neer wrote:
> thanx.
> 
> BTW, what is the simplest way to prove simple goals like "0<=2"?
> "fourier" works but I wonder if it is not an overkill.

The cheapest way is to define a coercion from Z to R and to prove that
it is a morphism for the comparison operators. Then you can do the
following:

Goal (1234 <= 2345)%R.
now apply (Z2R_le 1234 2345).
Qed.

You can find such a definition in the Flocq library for instance.

Best regards,

Guillaume