I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,
Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)
they show how to prove inequalities such as
[![Inequality][1]][1]
(from p.11 of the arXiv version.)