intervalArithmetic proves quantifier-free real arithmetic
when the antecedent has numerical bounds for all free variables of the succedent.
The tactic can be quite efficient but may fail in difficult cases.
See also
Tools → Cut Interval Bounds to compute interval bounds for given terms.