R. Affeldt, C. Cohen, A. Mahboubi, D. Rouhling, and P. Y. Strub, Analysis library 4 compatible with Mathematical Components. https://github, p.analysis, 2017.

J. Avigad and K. Donnelly, Formalizing O Notation in Isabelle/HOL, p.9
DOI : 10.1007/978-3-540-25984-8_27

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

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

C. Cohen and D. Rouhling, A Formal Proof in Coq of LaSalle's Invariance Princi- 22

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

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging mathematical 29 structures, Theo- 30 rem Proving in Higher Order Logics, 22nd International Conference Proceedings. Lecture Notes in Com- 32, 2009.
DOI : 10.1007/978-3-642-03359-9_23
URL : http://hal.archives-ouvertes.fr/docs/00/40/16/97/PDF/main.pdf

G. Gonthier, The Mathematical Components repository. https: 35 //github.com/math-comp/math-comp (2017), full list of contributors: https:// 36 github, p.37

A. Guéneau, A. Charguéraud, and F. Pottier, A fistful of dollars: Formalizing asymp- 38 totic complexity claims via deductive program verification, 27th European Sym- 39 posium on Programming, 2018.

J. Hölzl, F. Immler, and B. Huffman, Type Classes and Filters for Mathematical 41

E. Landau, Handbuch der Lehre von der Verteilung der, Primzahlen. B.G. Teubner, vol.46, p.47, 1909.

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, p.48
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:// 1 math-comp.github.io/mcb, 2016.

D. Rouhling, A Formal Proof in Coq of a Control Function for the Inverted Pen