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