A formalization of the Dedekind real numbers in Coq.

Structure of the modules:

• Cut: definition of Dedekind cuts and several other basic notions
• MiscLemmas: various lemmas about rational number
• Arithmetic: definitions and properties of arithmetical operations
• Lipschitz: definitions and facts about locally Lipschitz functions
• Archimedean: the proof that the reals satisfy the archimedean property