# Library Coq.Reals.Rlogic

This module proves some logical properties of the axiomatic of Reals.

- Decidability of arithmetical statements.
- Derivability of the Archimedean "axiom".
- Decidability of negated formulas.

# Decidability of arithmetical statements

Section Arithmetical_dec.

Variable P : nat -> Prop.

Hypothesis HP : forall n, {P n} + {~P n}.

Lemma sig_forall_dec : {n | ~P n} + {forall n, P n}.

End Arithmetical_dec.