fact: Structure ConstructiveReals : Type := { CRcarrier : Set; CRlt : CRcarrier -> CRcarrier -> Set; CRltLinear : isLinearOrder CRlt; CRle (x y : CRcarrier) := CRlt y x -> False; CReq (x y : CRcarrier) := CRle y x /\ CRle x y; CRapart (x y : CRcarrier) := sum (CRlt x y) (CRlt y x); CRltProp : CRcarrier -> CRcarrier -> Prop; CRltEpsilon : forall x y : CRcarrier, CRltProp x y -> CRlt x y; CRltForget : forall x y : CRcarrier, CRlt x y -> CRltProp x y; CRltDisjunctEpsilon : forall a b c d : CRcarrier, (CRltProp a b \/ CRltProp c d) -> CRlt a b + CRlt c d; CR_of_Q : Q -> CRcarrier; CR_of_Q_lt : forall q r : Q, Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); lt_CR_of_Q : forall q r : Q, CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; CRplus : CRcarrier -> CRcarrier -> CRcarrier; CRopp : CRcarrier -> CRcarrier; CRmult : CRcarrier -> CRcarrier -> CRcarrier; CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r)) (CRplus (CR_of_Q q) (CR_of_Q r)); CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r)) (CRmult (CR_of_Q q) (CR_of_Q r)); CRisRing : ring_theory (CR_of_Q 0) (CR_of_Q 1) CRplus CRmult (fun x y => CRplus x (CRopp y)) CRopp CReq; CRisRingExt : ring_eq_ext CRplus CRmult CRopp CReq; CRzero_lt_one : CRlt (CR_of_Q 0) (CR_of_Q 1); CRplus_lt_compat_l : forall r r1 r2 : CRcarrier, CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2); CRplus_lt_reg_l : forall r r1 r2 : CRcarrier, CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2; CRmult_lt_0_compat : forall x y : CRcarrier, CRlt (CR_of_Q 0) x -> CRlt (CR_of_Q 0) y -> CRlt (CR_of_Q 0) (CRmult x y); CRinv : forall x : CRcarrier, CRapart x (CR_of_Q 0) -> CRcarrier; CRinv_l : forall (r:CRcarrier) (rnz : CRapart r (CR_of_Q 0)), CReq (CRmult (CRinv r rnz) r) (CR_of_Q 1); CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r (CR_of_Q 0)), CRlt (CR_of_Q 0) r -> CRlt (CR_of_Q 0) (CRinv r rnz); CR_Q_dense : forall x y : CRcarrier, CRlt x y -> { q : Q & prod (CRlt x (CR_of_Q q)) (CRlt (CR_of_Q q) y) }; CR_archimedean : forall x : CRcarrier, { n : positive & CRlt x (CR_of_Q (Z.pos n # 1)) }; CRminus (x y : CRcarrier) : CRcarrier := CRplus x (CRopp y); CRabs : CRcarrier -> CRcarrier; CRabs_def : forall x y : CRcarrier, (CRle x y /\ CRle (CRopp x) y) <-> CRle (CRabs x) y; CR_cv (un : nat -> CRcarrier) (l : CRcarrier) : Set := forall p:positive, { n : nat | forall i:nat, le n i -> CRle (CRabs (CRminus (un i) l)) (CR_of_Q (1#p)) }; CR_cauchy (un : nat -> CRcarrier) : Set := forall p : positive, { n : nat | forall i j:nat, le n i -> le n j -> CRle (CRabs (CRminus (un i) (un j))) (CR_of_Q (1#p)) }; CR_complete : forall xn : (nat -> CRcarrier), CR_cauchy xn -> { l : CRcarrier & CR_cv xn l }; }.
imports: QArith Qabs Qround