T. W. Armstrong and G. Struth, Programming and automating mathematics in the Tarski???Kleene hierarchy, Journal of Logical and Algebraic Methods in Programming, vol.83, issue.2, 2014.
DOI : 10.1016/j.jlap.2014.02.001

Y. Bertot, G. Gonthier, S. O. Biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher-Order Logics, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

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

A. Chaieb, Formal Power Series, Journal of Automated Reasoning, vol.11, issue.1, pp.291-318, 2011.
DOI : 10.1007/s10817-010-9195-9

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

C. Cohen, Construction of Real Algebraic Numbers in Coq, 2012.
DOI : 10.1007/978-3-642-32347-8_6
URL : https://hal.archives-ouvertes.fr/hal-00671809

C. Cohen, Pragmatic Quotient Types in Coq, Interactive Theorem Proving, pp.213-228978
DOI : 10.1007/978-3-642-39634-2_17

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, Interactive Theorem Proving, pp.163-179978, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

A. Mahboubi, lstcoq.sty file which defines a Coq - SSReflect style for listings in Latex, 2015.

P. Quaresma, DCpic package to draw diagrams in Latex, 2015.

P. Strub, A Coq/Ssreflect Library for Elliptic Curves, Interactive Theorem Proving, pp.77-92, 2014.

. Wikipedia, Composition of series. https://en.wikipedia.org/wiki/Formal_power_series#Composition_of_ser Accessed, pp.29-35, 2015.