The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi

lra (linear real arithmetic) of Psatz does the job

Require Import Reals Psatz.

Open Scope R_scope.

Goal 1 / 3 <> 1.
lra.
Qed.


On 08/05/2016 11:18 AM, Daniel de Rauglaudre wrote:
> 2/ The immediate question that I have now is how to prove that the
>    hypothesis (1 / 3)%R = 1%R is contradictory? I tried discriminate,
>    discrR and other field_simplify. But I cannot manage to finish it
>    in a simple way. A research on google gave me nothing interesting
>    but perhaps I did not put the good terms.