Library Stdlib.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.
From Stdlib Require Import PeanoNat.
From Stdlib Require Import Zabs.
From Stdlib Require Import Zorder.
From Stdlib Require Import RIneq.
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.