This development is about termination proofs and ordinal numbers. It will also serve as a corpus for studying the relationship between Coq and the mathematical language. This work is still unfinished, and we hope it will remain so, as the doamin is very rich. Table of modules : prelude/ Some preliminary definitions and results (Pierre Castéran, Evelyne Contéjean) hilbert/ Introducing in Coq Hilbert's epsilon operator (Pierre Castéran) denumerable/ Denumerable sets (Florian Hatat) rpo/ About the recursive path ordering (Evelyne Contéjean) epsilon0/ Ordinals in Cantor Normal Form (Pierre Castéran) gamma0/ Ordinals in Veblen Normal Form (Pierre Castéran) schutte/ Axiomatic presentation of denumerable ordinals, after K. Schütte (Pierre Castéran) misc/ Computing the length of the Goodstein sequence starting from 4 (in base 2) (Pierre Castéran) SCHROEDER/ Slight modification of the contribution by Hugo Herbelin (Florian Hatat)