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 and tarski.