·. Grimm, Definition BQpair_aux2b C := forall n m, natp n -> natp m -> P (Vg C n) <q Q (Vg C m)

A. Important, every Cauchy sequence has a limit Consider first a Cauchy sequence of rational numbers y. Let B be the set of all t ? Q such that, for some N , y n < t when n ? N . If B has a least element b, then b is the limit of the sequence y. Otherwise B is a real number (note that B is non-empty since the sequence y is bounded), and is the limit of y. Let x be a real Cauchy sequence. We can find (via the axiom of choice) a sequence of rational numbers y such that |x n ? y n This sequence is then Cauchy

R. Boldo, C. Lelay, and G. Melquiond, Formalization of real analysis: a survey of proof assistants and libraries, Mathematical Structures in Computer Science, vol.11, issue.07, p.38, 2014.
DOI : 10.1007/3-540-44755-5_5
URL : https://hal.archives-ouvertes.fr/hal-00806920

]. N. Bou68, . Bourbakibou70-]-n, and . Bourbaki, Theory of Sets Éléments de mathématiques, Théorie des ensembles. Diffusion CCLS Translation of the, Elements of MathematicsBou89a] N. Bourbaki. Elements of Mathematics, Algebra I Elements of Mathematics, General Topology, 1966.

G. Cantor, Contributions to the Founding of the Theory of Transfinite Numbers, Trans. P. Jourdain, 1897.

C. Cohen, Construction of Real Algebraic Numbers in Coq, ITP -3rd International Conference on Interactive Theorem Proving -2012, 2012.
DOI : 10.1007/978-3-642-32347-8_6
URL : https://hal.archives-ouvertes.fr/hal-00671809

W. Edsger, . R. Dijkstra-dr, and . Burstall, An exercise for Available at http://www.cs.utexas, 1976.

W. Edsger and . Dijkstra, More about the function " fusc " (a sequel to EWD570) Available at http://www.cs.utexas, GGMR09] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures Theorem Proving in Higher Order Logics, 1976.

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 1979.
URL : https://hal.archives-ouvertes.fr/inria-00515548

J. Grimm, Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers, 2009.

J. Grimm, Implementation of Bourbaki's Elements of Mathematics in Coq, part one theory of sets, Journal of Formalized Reasoning, vol.3, issue.1, pp.79-126, 2010.

J. Grimm, Fibonacci numbers and the Stern-Brocot tree in Coq, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01093589

M. Niqui and Y. Bertot, QArith: Coq Formalisation of Lazy Rational Arithmetic, Types for Proofs and Programs, pp.309-323, 2004.
DOI : 10.1007/978-3-540-24849-1_20
URL : https://hal.archives-ouvertes.fr/inria-00077041

M. Simpson, Exact arithmetic on the Stern-Brocot tree Computer theorem proving in math, Journal of Discrete Algorithms, vol.5, issue.2, 2004.

C. Simpson, C. Laboratoire, and J. A. Dieudonne, Set-theorical mathematics in Coq arXiv:math/0402336v1, Ste58] Moritz Stern. Ueber eine zahlentheorische Funktion. Journal für die reine und angewandte Mathematik, pp.193-220, 1858.