G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Special Issue on Logical Frameworks and Met- alanguages, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501

URL : https://hal.archives-ouvertes.fr/hal-01124972

A. Bostan, Algorithmique efficace pour des opérations de base en Calcul formel, 2003.

C. Cohen, Types quotients en coq Actes des 21ème journées francophones des langages applicatifs, 2010.

C. Cohen and T. Coquand, A constructive version of Laplace's proof on the existence of complex roots

C. Cohen and A. Mahboubi, Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Logical Methods in Computer Science, vol.8, issue.1, pp.1-40, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00593738

D. Delahaye, A Tactic Language for the System Coq, Lecture Notes in Computer ScienceLNCS)Lecture Notes in Artificial Intelligence (LNAI), vol.1955, pp.85-95, 2000.
DOI : 10.1007/3-540-44404-1_7

URL : https://hal.archives-ouvertes.fr/hal-01125070

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Lecture Notes in Computer Science, vol.1, issue.258, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11

URL : https://hal.archives-ouvertes.fr/inria-00368403

H. Geuvers and M. Niqui, Constructive reals in coq: Axioms and categoricity. In: Selected papers from the International Workshop on Types for Proofs and Programs, TYPES '00, pp.79-95, 2002.

R. Krebbers and B. Spitters, Computer Certified Efficient Exact Reals in Coq, Conference on Intelligent Computer Mathematics, CICM 2011 Proceedings. Lecture Notes in Artifical Intelligence, 2011.
DOI : 10.1007/978-3-642-04027-6_12

S. Lang, Algebra. Graduate texts in mathematics, 2002.

R. Mines, F. Richman, and W. Ruitenburg, A course in constructive algebra, Universitext, 1979.
DOI : 10.1007/978-1-4419-8640-5

O. Connor and R. , Certified exact transcendental real number computation in coq, Theorem Proving in Higher Order Logics, pp.246-261978, 2008.

T. M. Project, SSReflect extension and libraries. http://www.msr-inria. inria