We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge,
this is the first generally useful proof-producing implementation of such an algorithm. While many problems within the domain
are intractable, we demonstrate convincing examples of its value in interactive theorem proving.