C. Affeldt, A. Cohen, D. Mahboubi, P. Rouhling, and . Strub, Analysis library compatible with Mathematical Components . https://github.com/math-comp/analysis/tree/asymptotic_reasoning_ paper Work in progress, 2018.

J. Avigad and K. Donnelly, Formalizing O Notation in Isabelle/HOL, Automated Reasoning -Second International Joint Conference Proceedings, pp.357-371, 2004.
DOI : 10.1007/978-3-540-25984-8_27

J. Arnaudiès and H. Fraysse, Analyse. Dunod, vol.2, 1988.

P. Bachmann, . B. Die-analytische-zahlentheorie, and . Teubner, , 1894.

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, pp.41-62, 2015.
DOI : 10.1109/32.713327
URL : https://hal.archives-ouvertes.fr/hal-00860648

S. Boldo, C. Lelay, and G. Melquiond, The Coquelicot library Available at: http://coquelicot.saclay.inria.fr, 2017.

S. Blazy, C. Paulin-mohring, and D. Pichardie, Interactive Theorem Proving -4th International Conference Proceedings, volume 7998 of Lecture Notes in Computer Science, 2013.

C. Cohen, Formalized algebraic numbers: construction and first-order theory, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

, 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, Interactive Theorem Proving -8th International Conference, ITP 2017 Proceedings, volume 10499 of Lecture Notes in Computer Science, pp.148-163, 2017.
DOI : 10.1007/978-3-540-71067-7_20

M. Eberl, Proving Divide and Conquer Complexities in Isabelle/HOL, Journal of Automated Reasoning, vol.60, issue.3, pp.483-508, 2017.
DOI : 10.1007/978-3-642-12251-4_9

G. Gonthier, The Mathematical Components repository. https://github. com/math-comp/math-comp, 2018. Full list of contributors: https://github, Project started, 2006.

A. Guéneau, A. Charguéraud, and F. Pottier, A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification, Programming Languages and Systems -27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software Proceedings, volume 10801 of Lecture Notes in Computer Science, pp.533-560, 2018.
DOI : 10.1145/361002.361016

[. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Theorem Proving in Higher Order Logics, 22nd International Conference Proceedings, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

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

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system, 2016.
URL : https://hal.archives-ouvertes.fr/inria-00258384

[. Hölzl, F. Immler, and B. Huffman, Type Classes and Filters for Mathematical Analysis in Isabelle/HOL, Blazy et al. [BPP13], pp.279-294

E. Donald and . Knuth, Letter to the editor of the Notices of the, 1998.

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

, Lean mathematical components library. https://github.com/leanprover/mathlib, 2018.

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, Blazy et al. [BPP13], pp.19-34
DOI : 10.1007/978-3-642-39634-2_5
URL : https://hal.archives-ouvertes.fr/hal-00816703

A. Mahboubi and E. Tassi, Mathematical Components Available at: https: //math-comp.github.io/mcb, With contributions by Yves Bertot and Georges Gonthier, 2016.

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

, The Univalent Foundations Program Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, 2013.