The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

I'll assume that you're dealing with Z integers (otherwise you wouldnt
write such bignumbers without crashing Coq anyway :)). Since
comparison on Z is computable (and defined as a function) and your
expression is ground, (vm_compute; intro; discriminate) should do the
trick in principle. Similary, for goals involving strict comparisons,
you can use reflexivity.

Now, in your case, the inequality is False so there's no way you will
be able to prove that. Try vm_compute and you will see that the goal
reduces to Gt=Gt -> False which is not provable. The reason for that
is that the first operand of the sum is 0 (euclidian division) and the
second is -1 (which can be surprising but thats the way it is defined
for negative integers in the standard library). Try the division in
ZOdiv for a more "intuitive" result maybe.

HTH,

Stéphane L.

On Thu, Mar 12, 2009 at 4:26 PM, Eric Biagioli 
<ericbiagioli AT gmail.com>
 wrote:
> Hello everyone,
>
> I'm writing to ask a little question. I'm sorry if it's a stupid
> question. I need to prove (in Coq) that
>
> 0 <= 87500000020642221/100000000000000000+ -1/1000
>
> The "fourier" tactic didn't work (perhaps I'm doing something wrong?),
> and I don't know what could I do.
>
> Thankyou in advance,
>
> Eric
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06