As an example for both results and proof-techniques in computable reverse
mathematics, a proof is given that the intermediate value theorem is not
idempotent. This means that we it is impossible to solve two instances of the
intermediate value theorem using a solution of a single instance together with
computable means.
The proof techniques we use apply to choice principles in general, these are
multi-valued functions mapping negative information about closed sets to members
of the sets. As choice principles seem to be ubiquitous in computable reverse
mathematics, the techniques are promising to be useful in many more cases.