The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Stéphane Lescuyer a écrit :
> To prove it "manually", try multiplying both sides by the big
> (positive) denumerator (Rmult_le_reg_l willbe your friend) and
> simplify in order to end up with an inequality that  automatic tactics
> can handle.

Such simplification can be done by field_simplify. Try e.g.
field_simplifiy (87500000020642221 / 100000000000000000 + -1 / 1000).
Then use lemma Rmult_le_reg_l, field_simplify again and then fourier 
should apply (last hint: prove x/1=x with field).

Not as automated as one would expect indeed. Feedback on common 
situations where using field is painful (like this one) is welcome, as 
it will help us improve field.

In the meantime, crafting a small Ltac script that does it automatically 
is a good exercise and will improve your proof script. (I guess Adam 
Chlipala will agree.)

Bruno Barras.