We prove constructively (in the style of Bishop) that every monotone
continuous function with a lower bound on its slope has a continuous
inverse. The proof is formalized, and a realizing term extracted.
This term can be applied to concrete continuous functions and
arguments, and then normalized to a rational approximation of
say a zero of a given function. It turns out that even in
the logical term language `normalization by evaluation}'is reasonably