Recently Stefan Gerhold and Manuel Kauers introduced a new approach for algorithmically proving inequalities involving a discrete parameter. The proof then proceeds by induction along this discrete parameter, where the proof of the induction step is carried out using cylindrical algebraic decomposition (CAD). This is the first-and to this day only-practical method available for applying computer algebra to proving special functions inequalities. In this talk we introduce this approach and present two recent results obtained by it. First a direct application: the proof of a positivity conjecture by Joachim Sch\"oberl that arose in the construction of a new, stable interpolation operator for high order finite element methods. Second a variant of the Gerhold/Kauers approach: an automated way to sharpen classical estimates such as Wallis' inequality on approximating sequences for pi. The latter is joint work with Peter Paule.