The Coq mailing list

[David MENTRE <dmentre AT linux-france.org>]

Hello Frédéric,

Le 5 avril 2012 10:02, Frédéric Besson 
<frederic.besson AT inria.fr>
 a écrit :
> Here is the way I would do it:
> * Get rid of Rdiv and Rinv.
> * Use (available) decision procedures to discharge the rest
>
> Here is the whole script.

Thanks a lot for the script. Unfortunately such Ltac definitions are a
bit complex for me to understand right now. :-)

Best regards,
d.