  The aim of this paper is to present a new algorithm for proving mixed
trigonometric-polynomial inequalities by reducing to polynomial inequalities.
Finally, we show the great applicability of this algorithm and as examples, we
use it to analyze some new rational (Pade) approximations of the function
$\cos^2(x)$, and to improve a class of inequalities by Z.-H. Yang. The results
of our analysis could be implemented by means of an automated proof assistant,
so our work is a contribution to the library of automatic support tools for
proving various analytic inequalities.
