This library provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant. Homepage: http://coq-interval.gforge.inria.fr/
