Real closed fields for Mathematical Components

 This library contains definitions and theorems about real closed fields
 for Mathematical Components. It includes a construction of the real
 and algebraic closure (with a proof of the fundamental theorem of
 algebra). The decidability of the first order theory of real closed
 field, through quantifier elimination is also established.
 .
 The Mathematical Components library is a coherent repository of
 general-purpose formalized mathematical theories for the
 Coq proof assistant.