The aim of this paper is to present a new algorithm for proving mixed trigonometric-polynomial inequalities of the form $$\sum_{i=1}^{n}\alpha _{i}x^{p_{i}} \cos ^{q_{i}} x\sin ^{r_{i}} x>0 $$ by reducing them to polynomial inequalities. Finally, we show the great applicability of this algorithm and, as an example, we use it to analyze some new rational (Padé) approximations of the function cos² x and to improve a class of inequalities by 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.

In this paper we propose a new method for sharpening and refinements of some trigonometric inequalities. We apply these ideas to some inequalities of Wilker–Cusa–Huygens type.

In this paper, we give some sharper refinements and generalizations of inequalities related to Shafer-Fink’s inequality for the inverse sine function stated in Theorems 1, 2, and 3 of Bercu (Math. Probl. Eng. 2017: Article ID 9237932, 2017).