Library mathcomp.real_closed.all_real_closed

Require Export bigenough.
Require Export cauchyreals.
Require Export complex.
Require Export ordered_qelim.
Require Export polyorder.
Require Export polyrcf.
Require Export qe_rcf_th.
Require Export qe_rcf.
Require Export realalg.
Require Export mxtens.