# Library Coq.Reals.ConstructiveRcomplete

Require Import QArith_base.
Require Import Qabs.
Require Import ConstructiveCauchyReals.
Require Import Logic.ConstructiveEpsilon.

Local Open Scope CReal_scope.

Lemma CReal_absSmall : forall (x y : CReal) (n : positive),
(Qlt (2 # n)
(proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n))))
-> (CRealLt (CReal_opp x) y * CRealLt y x).

Definition absSmall (a b : CReal) : Set
:= -b < a < b.

Definition Un_cv_mod (un : nat -> CReal) (l : CReal) : Set
:= forall n : positive,
{ p : nat & forall i:nat, le p i -> absSmall (un i - l) (IQR (1#n)) }.

Lemma Un_cv_mod_eq : forall (v u : nat -> CReal) (s : CReal),
(forall n:nat, u n == v n)
-> Un_cv_mod u s -> Un_cv_mod v s.

Definition Un_cauchy_mod (un : nat -> CReal) : Set
:= forall n : positive,
{ p : nat & forall i j:nat, le p i
-> le p j
-> -IQR (1#n) < un i - un j < IQR (1#n) }.

Fixpoint Rfloor_pos (a : CReal) (n : nat) { struct n }
: 0 < a
-> a < INR n
-> { p : nat & INR p < a < INR p + 2 }.

Definition Rfloor (a : CReal)
: { p : Z & IZR p < a < IZR p + 2 }.

Definition Rup_nat (x : CReal)
: { n : nat & x < INR n }.

Definition FQ_dense_pos (a b : CReal)
: 0 < b
-> a < b -> { q : Q & a < IQR q < b }.

Definition FQ_dense (a b : CReal)
: a < b
-> { q : Q & a < IQR q < b }.

Definition RQ_limit : forall (x : CReal) (n:nat),
{ q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }.

Definition Un_cauchy_Q (xn : nat -> Q) : Set
:= forall n : positive,
{ k : nat | forall p q : nat, le k p -> le k q
-> Qlt (-(1#n)) (xn p - xn q)
/\ Qlt (xn p - xn q) (1#n) }.

Lemma Rdiag_cauchy_sequence : forall (xn : nat -> CReal),
Un_cauchy_mod xn
-> Un_cauchy_Q (fun n => let (l,_) := RQ_limit (xn n) n in l).

Lemma doubleLtCovariant : forall a b c d e f : CReal,
a == b -> c == d -> e == f
-> (a < c < e)
-> (b < d < f).

Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> nat),
QSeqEquiv qn (fun n => proj1_sig x n) cvmod
-> Un_cv_mod (fun n => IQR (qn n)) x.

Lemma Un_cv_extens : forall (xn yn : nat -> CReal) (l : CReal),
Un_cv_mod xn l
-> (forall n : nat, xn n == yn n)
-> Un_cv_mod yn l.

Lemma R_has_all_rational_limits : forall qn : nat -> Q,
Un_cauchy_Q qn
-> { r : CReal & Un_cv_mod (fun n => IQR (qn n)) r }.

Lemma Rcauchy_complete : forall (xn : nat -> CReal),
Un_cauchy_mod xn
-> { l : CReal & Un_cv_mod xn l }.