README.md

A formalization of the Dedekind real numbers in Coq.

Structure of the modules:

• MiscLemmas: various lemmas about rational number
• Cut: definition of Dedekind cuts and several other basic notions
• Additive: Additive structure of the reals
• Multiplication : Multiplicative structure of the relas
• Order : The order on the reals
• Archimedean: the proof that the reals satisfy the archimedean property
• Completeness: the reals are Dedekind-complete