R. Aeldt, C. Cohen, A. Mahboubi, D. Rouhling, P. Strub-;-reynald-aeldt et al., Classical analysis with Coq, Analysis library compatible with Mathematical Components, 2018.

J. Avigad and K. Donnelly, Formalizing O notation in Isabelle/HOL, Proceedings of the Second International Joint Conference on Automated Reasoning, vol.3097, p.357371, 2004.

J. , M. Arnaudiès, and H. Fraysse, Cours de mathématiques, Analyse. Dunod, vol.2, 1988.

, Proceedings of the 8th International Conference on Interactive Theorem Proving, vol.10499, 2017.

P. Bachmann, Die Analytische Zahlentheorie. B.G. Teubner, 1894

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.50, issue.4, p.423456, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00649240

S. Bernard, Formalization of the Lindemann-Weierstrass theorem, Ayala-Rincón and Muñoz, p.6580
URL : https://hal.archives-ouvertes.fr/hal-01647563

. Coqapprox,

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, p.4162, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00860648

S. Boldo, C. Lelay, and G. Melquiond, The Coquelicot library, 2018.

S. Blazy, C. Paulin-mohring, and D. Pichardie, Proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, 2013.

C. Cohen, Construction of real algebraic numbers in Coq, Proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, vol.7406, p.6782, 1315.
URL : https://hal.archives-ouvertes.fr/hal-00671809

C. Cohen, Formalized algebraic numbers: construction and rstorder theory, 2012.

, The Coq Development Team. The Coq proof assistant reference manual, 2018.

C. Cohen and D. Rouhling, A Formal Proof in Coq of LaSalle's Invariance Principle, vol.148, p.163

R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society, vol.51, p.176178, 1975.

M. Eberl, Proving divide and conquer complexities in Is

/. Hol, Journal of Automated Reasoning, vol.58, issue.4, p.483508, 2017.

G. Gonthier, The Mathematical Components repository

G. Gonthier, A. Asperti, and J. Avigad,

F. Cohen, S. Garillot, A. Le-roux, . Mahboubi, O. Russell et al., A Machine-Checked Proof of the Odd Order Theorem, vol.13, p.163179
URL : https://hal.archives-ouvertes.fr/hal-00816699

A. Guéneau, A. Charguéraud, and F. Pottier, A stful of dollars: Formalizing asymptotic complexity claims via deductive program verication, Proceedings of the 27th European Symposium on Programming on Programming Languages and Systems, ESOP 2018, held as part of the European Joint Conferences on Theory and Practice of Software, vol.2018, p.533560, 1420.

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging mathematical structures, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, vol.5674, p.327342, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00368403

G. Gonthier and A. Mahboubi, An introduction to small scale reection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, p.95152, 2010.

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reection Extension for the Coq system, 2016.

G. Gonthier, Point-free, set-free concrete linear algebra, Proceeding of the 2nd International Conference on Interactive Theorem Proving, vol.6898, pp.103-118, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00805966

A. Guéneau, Procrastination, a proof engineering technique, Coq Workshop, 2018.

J. Hölzl, F. Immler, and B. Human, Type Classes and Filters for Mathematical Analysis in Isabelle/HOL, vol.13, p.279294

D. E. Knuth, Teach Calculus with Big O. Notices of the AMS, vol.45, p.687688, 1998.

E. Landau,

, Handbuch der Lehre von der Verteilung der Primzahlen, 1909.

, The Lean mathematical components library developers. Lean mathematical components library

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, vol.13, p.1934
URL : https://hal.archives-ouvertes.fr/hal-00816703

A. Mahboubi and E. Tassi,

, Mathematical Components. Available

D. Rouhling, A Formal Proof in Coq of a Control Function for the Inverted Pendulum, Proceedings of the 7th ACM SIGPLAN International Conference on Certied Programs and Proofs, vol.2018, p.2841, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01639819

D. Schepler, coq-topology: Topology library for Coq, 2011.

D. Schepler, coq-zorns-lemma: Naive set theory library for Coq, 2011.

M. Sozeau and N. Oury, First-class type classes, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs, vol.5170, p.278293, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00628864

, The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.