The Coq mailing list

["Pierre.ABBRUGIATI" <abbrugia AT math.unice.fr>]

Dear Coq-Club,

Apologies for my pityful english (french message following).

Can one study the variations of of real function in Coq ?
ie : can one prove that a real function is (strictly) monotonous on a 
given interval ?
My problem is the following : I would like to prove the function x -> 
ln(x)/x is strictly decreasing on ]e,+infinity[.
(maybe I need a stronger version of |negative_derivative| ? although I 
may not be able to prove that (ln(x)/x)' = (1-ln(x))/x^2... :'()

Thanks a lot,
Pierre Abbrugiati.

*************************************************

Bonjour,

Peut-on étudier les variations d'une fonction réelle en Coq ?
C'est à dire : peut-on établir qu'une fonction réelle est (strictement) 
monotone sur un intervalle donné (autre que R) ?
Mon exemple est le suivant : j'aimerais montrer que la fonction x -> 
ln(x)/x est strictement décroissante sur ]e, +infini[.
(j'aurais donc peut-être besoin d'une version adaptée de 
|negative_derivative| ? ...quoique, a priori, je ne suis même pas 
capable de prouver que la dérivée de ma fonction est bien 
(1-ln(x))/x^2... :'()

D'avance, merci beaucoup.
Pierre Abbrugiati.