# [isabelle] unknow theorem

Hello
I am using the HOL-Complex logic and I want to prove
[| 0 <= Lb X; 0 <= Lb Y; Lb X <= x; x <= Ub X; Lb Y <= y; y <= Ub Y |]
==> Lb X * Lb Y <= x * y
where all terms are of type real.
I find the lemma "mult_mono" in the Ring_and_Field theory of HOL logic,
(at http://www.cl.cam.ac.uk/~lp15/Isabelle/dist/library/HOL/Ring_and_Field.html)
but when I tried to use it, isabelle answers:
*** Error in method "HOL.rule":
*** Unknown theorem(s) "mult_mono"
*** At command "apply".
How can I do for use that theorem? Where can I find the theorems for prove
inequalities of reals?
Thanks
Francisco
-- Francisco José Cháves (ENS-LIP)
mailto: Francisco.Jose.Chaves.Alonso at ens-lyon.fr
http://perso.ens-lyon.fr/francisco.jose.chaves.alonso
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*