Hypatheon is useful for browsing libraries. In the Prelude, we have real_axioms, reals and real_props. For example, in real_props we have the Lemma “both_sides_div_pos_neg_ge1” which allows us to divide both sides of an inequality x >= y by the same value n0z: VAR nonzero_real:

Lemma is: FORALL (n0z: nonzero_real, x, y: real):
         IF n0z > 0 THEN x/n0z >= y/n0z ELSE y/n0z >= x/n0z ENDIF
         IFF x >= y

This can be used to show, e.g. that x*x >= x.

There are also libraries of decision procedures such as

• sturm: Sturm's Theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, and is included in the NASA PVS libraries.
• tarski.Tarski's Theorem is a generalization of Sturm's theorem that provides a linear relationship between functions known as Tarski queries and cardinalities of certain sets. It's also in the NASA library.