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.