Library Coq.Reals.ConstructiveCauchyReals


Require Import QArith.
Require Import Qabs.
Require Import Qround.
Require Import Logic.ConstructiveEpsilon.
Require CMorphisms.

Open Scope Q.

Definition QSeqEquiv (un vn : nat -> Q) (cvmod : positive -> nat)
  : Prop
  := forall (k : positive) (p q : nat),
      le (cvmod k) p
      -> le (cvmod k) q
      -> Qlt (Qabs (un p - vn q)) (1 # k).

Definition QCauchySeq (un : nat -> Q) (cvmod : positive -> nat) : Prop
  := QSeqEquiv un un cvmod.

Lemma QSeqEquiv_sym : forall (un vn : nat -> Q) (cvmod : positive -> nat),
    QSeqEquiv un vn cvmod
    -> QSeqEquiv vn un cvmod.

Lemma factorDenom : forall (a:Z) (b d:positive), (a # (d * b)) == (1#d) * (a#b).

Lemma QSeqEquiv_trans : forall (un vn wn : nat -> Q)
                          (cvmod cvmodw : positive -> nat),
    QSeqEquiv un vn cvmod
    -> QSeqEquiv vn wn cvmodw
    -> QSeqEquiv un wn (fun q => max (cvmod (2 * q)%positive) (cvmodw (2 * q)%positive)).

Definition QSeqEquivEx (un vn : nat -> Q) : Prop
  := exists (cvmod : positive -> nat), QSeqEquiv un vn cvmod.

Lemma QSeqEquivEx_sym : forall (un vn : nat -> Q), QSeqEquivEx un vn -> QSeqEquivEx vn un.

Lemma QSeqEquivEx_trans : forall un vn wn : nat -> Q,
    QSeqEquivEx un vn
    -> QSeqEquivEx vn wn
    -> QSeqEquivEx un wn.

Lemma QSeqEquiv_cau_r : forall (un vn : nat -> Q) (cvmod : positive -> nat),
    QSeqEquiv un vn cvmod
    -> QCauchySeq vn (fun k => cvmod (2 * k)%positive).

Fixpoint increasing_modulus (modulus : positive -> nat) (n : nat)
  := match n with
     | O => modulus xH
     | S p => max (modulus (Pos.of_nat n)) (increasing_modulus modulus p)
     end.

Lemma increasing_modulus_inc : forall (modulus : positive -> nat) (n p : nat),
    le (increasing_modulus modulus n)
       (increasing_modulus modulus (p + n)).

Lemma increasing_modulus_max : forall (modulus : positive -> nat) (p n : nat),
    le n p -> le (modulus (Pos.of_nat n))
                 (increasing_modulus modulus p).

Lemma standard_modulus : forall (un : nat -> Q) (cvmod : positive -> nat),
    QCauchySeq un cvmod
    -> (QCauchySeq (fun n => un (increasing_modulus cvmod n)) Pos.to_nat
       /\ QSeqEquiv un (fun n => un (increasing_modulus cvmod n))
                   (fun p => max (cvmod p) (Pos.to_nat p))).

Definition CReal : Set
  := { x : (nat -> Q) | QCauchySeq x Pos.to_nat }.


Delimit Scope CReal_scope with CReal.


Open Scope CReal_scope.

Definition CRealLt (x y : CReal) : Set
  := { n : positive | Qlt (2 # n)
                           (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) }.

Definition CRealLtProp (x y : CReal) : Prop
  := exists n : positive, Qlt (2 # n)
                         (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)).

Definition CRealGt (x y : CReal) := CRealLt y x.
Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x).

Infix "<" := CRealLt : CReal_scope.
Infix ">" := CRealGt : CReal_scope.
Infix "#" := CReal_appart : CReal_scope.

Lemma CRealLtEpsilon : forall x y : CReal,
    CRealLtProp x y -> x < y.

Lemma CRealLtForget : forall x y : CReal,
    x < y -> CRealLtProp x y.

Lemma CRealLt_lpo_dec : forall x y : CReal,
    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
                    -> {n | ~P n} + {forall n, P n})
    -> CRealLt x y + (CRealLt x y -> False).

Definition CRealEq (x y : CReal) : Prop
  := (CRealLt x y -> False) /\ (CRealLt y x -> False).

Infix "==" := CRealEq : CReal_scope.

Definition CRealLe (x y : CReal) : Prop
  := CRealLt y x -> False.

Definition CRealGe (x y : CReal) := CRealLe y x.

Infix "<=" := CRealLe : CReal_scope.
Infix ">=" := CRealGe : CReal_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : CReal_scope.
Notation "x <= y < z" := (prod (x <= y) (y < z)) : CReal_scope.
Notation "x < y < z" := (prod (x < y) (y < z)) : CReal_scope.
Notation "x < y <= z" := (prod (x < y) (y <= z)) : CReal_scope.

Lemma CRealLe_not_lt : forall x y : CReal,
    (forall n:positive, Qle (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))
                       (2 # n))
    <-> x <= y.

Lemma CRealEq_diff : forall (x y : CReal),
    CRealEq x y
    <-> forall n:positive, Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n)))
                        (2 # n).

Lemma CRealEq_modindep : forall (x y : CReal),
    QSeqEquivEx (proj1_sig x) (proj1_sig y)
    <-> forall n:positive,
      Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) (2 # n).

Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive),
    (Qlt (2 # n)
         (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)))
    -> let (k, _) := Qarchimedean (/(proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n) - (2#n)))
      in forall p:positive,
          Pos.le (Pos.max n (2*k)) p
          -> Qlt (2 # (Pos.max n (2*k)))
                (proj1_sig y (Pos.to_nat p) - proj1_sig x (Pos.to_nat p)).

Lemma CRealLt_above : forall (x y : CReal),
    CRealLt x y
    -> { k : positive | forall p:positive,
          Pos.le k p -> Qlt (2 # k) (proj1_sig y (Pos.to_nat p) - proj1_sig x (Pos.to_nat p)) }.

Lemma CRealLt_above_same : forall (x y : CReal) (n : positive),
    Qlt (2 # n)
        (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n))
    -> forall p:positive, Pos.le n p
                    -> Qlt (proj1_sig x (Pos.to_nat p)) (proj1_sig y (Pos.to_nat p)).

Lemma CRealLt_asym : forall x y : CReal, x < y -> x <= y.

Lemma CRealLt_irrefl : forall x:CReal, x < x -> False.

Lemma CRealLe_refl : forall x : CReal, x <= x.

Lemma CRealEq_refl : forall x : CReal, x == x.

Lemma CRealEq_sym : forall x y : CReal, CRealEq x y -> CRealEq y x.

Lemma CRealLt_dec : forall x y z : CReal,
    CRealLt x y -> CRealLt x z + CRealLt z y.

Definition linear_order_T x y z := CRealLt_dec x z y.

Lemma CRealLe_Lt_trans : forall x y z : CReal,
    x <= y -> y < z -> x < z.

Lemma CRealLt_Le_trans : forall x y z : CReal,
    x < y -> y <= z -> x < z.

Lemma CRealLe_trans : forall x y z : CReal,
    x <= y -> y <= z -> x <= z.

Lemma CRealLt_trans : forall x y z : CReal,
    x < y -> y < z -> x < z.

Lemma CRealEq_trans : forall x y z : CReal,
    CRealEq x y -> CRealEq y z -> CRealEq x z.

Add Parametric Relation : CReal CRealEq
    reflexivity proved by CRealEq_refl
    symmetry proved by CRealEq_sym
    transitivity proved by CRealEq_trans
      as CRealEq_rel.

Instance CRealEq_relT : CRelationClasses.Equivalence CRealEq.

Instance CRealLt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealLt.

Instance CRealGt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealGt.

Instance CReal_appart_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CReal_appart.

Add Parametric Morphism : CRealLe
    with signature CRealEq ==> CRealEq ==> iff
      as CRealLe_morph.

Add Parametric Morphism : CRealGe
    with signature CRealEq ==> CRealEq ==> iff
      as CRealGe_morph.

Lemma CRealLt_proper_l : forall x y z : CReal,
    CRealEq x y
    -> CRealLt x z -> CRealLt y z.

Lemma CRealLt_proper_r : forall x y z : CReal,
    CRealEq x y
    -> CRealLt z x -> CRealLt z y.

Lemma CRealLe_proper_l : forall x y z : CReal,
    CRealEq x y
    -> CRealLe x z -> CRealLe y z.

Lemma CRealLe_proper_r : forall x y z : CReal,
    CRealEq x y
    -> CRealLe z x -> CRealLe z y.


Lemma ConstCauchy : forall q : Q,
    QCauchySeq (fun _ => q) Pos.to_nat.

Definition inject_Q : Q -> CReal.

Notation "0" := (inject_Q 0) : CReal_scope.
Notation "1" := (inject_Q 1) : CReal_scope.

Lemma CRealLt_0_1 : CRealLt (inject_Q 0) (inject_Q 1).

Lemma CReal_injectQPos : forall q : Q,
    Qlt 0 q -> CRealLt (inject_Q 0) (inject_Q q).

Lemma CRealLtQ : forall (x : CReal) (q : Q),
    CRealLt x (inject_Q q)
    -> forall p:positive, Qlt (proj1_sig x (Pos.to_nat p)) (q + (1#p)).

Lemma CRealLtQopp : forall (x : CReal) (q : Q),
    CRealLt (inject_Q q) x
    -> forall p:positive, Qlt (q - (1#p)) (proj1_sig x (Pos.to_nat p)).


Lemma CReal_plus_cauchy
  : forall (xn yn zn : nat -> Q) (cvmod : positive -> nat),
    QSeqEquiv xn yn cvmod
    -> QCauchySeq zn Pos.to_nat
    -> QSeqEquiv (fun n:nat => xn n + zn n) (fun n:nat => yn n + zn n)
                (fun p => max (cvmod (2 * p)%positive)
                           (Pos.to_nat (2 * p)%positive)).

Definition CReal_plus (x y : CReal) : CReal.

Infix "+" := CReal_plus : CReal_scope.

Lemma CReal_plus_nth : forall (x y : CReal) (n : nat),
    proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%nat) (proj1_sig y (2*n)%nat).

Lemma CReal_plus_unfold : forall (x y : CReal),
    QSeqEquiv (proj1_sig (CReal_plus x y))
              (fun n : nat => proj1_sig x n + proj1_sig y n)%Q
              (fun p => Pos.to_nat (2 * p)).

Definition CReal_opp (x : CReal) : CReal.

Notation "- x" := (CReal_opp x) : CReal_scope.

Definition CReal_minus (x y : CReal) : CReal
  := CReal_plus x (CReal_opp y).

Infix "-" := CReal_minus : CReal_scope.

Lemma belowMultiple : forall n p : nat, lt 0 p -> le n (p * n).

Lemma CReal_plus_assoc : forall (x y z : CReal),
    CRealEq (CReal_plus (CReal_plus x y) z)
            (CReal_plus x (CReal_plus y z)).

Lemma CReal_plus_comm : forall x y : CReal,
    x + y == y + x.

Lemma CReal_plus_0_l : forall r : CReal,
    CRealEq (CReal_plus (inject_Q 0) r) r.

Lemma CReal_plus_0_r : forall r : CReal,
    r + 0 == r.

Lemma CReal_plus_lt_compat_l :
  forall x y z : CReal,
    CRealLt y z
    -> CRealLt (CReal_plus x y) (CReal_plus x z).

Lemma CReal_plus_lt_reg_l :
  forall x y z : CReal, x + y < x + z -> y < z.

Lemma CReal_plus_lt_reg_r :
  forall x y z : CReal, y + x < z + x -> y < z.

Lemma CReal_plus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.

Lemma CReal_plus_le_lt_compat :
  forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.

Lemma CReal_plus_opp_r : forall x : CReal,
    x + - x == 0.

Lemma CReal_plus_opp_l : forall x : CReal,
    - x + x == 0.

Lemma CReal_plus_proper_r : forall x y z : CReal,
    CRealEq x y -> CRealEq (CReal_plus x z) (CReal_plus y z).

Lemma CReal_plus_proper_l : forall x y z : CReal,
    CRealEq x y -> CRealEq (CReal_plus z x) (CReal_plus z y).

Add Parametric Morphism : CReal_plus
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_plus_morph.

Instance CReal_plus_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_plus.

Lemma CReal_plus_eq_reg_l : forall (r r1 r2 : CReal),
    CRealEq (CReal_plus r r1) (CReal_plus r r2)
    -> CRealEq r1 r2.

Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) { struct k }
  : (forall n:nat, le k n -> Qlt (Qabs (qn n)) (Z.pos A # 1))
    -> { B : positive | forall n:nat, Qlt (Qabs (qn n)) (Z.pos B # 1) }.

Lemma QCauchySeq_bounded (qn : nat -> Q) (cvmod : positive -> nat)
  : QCauchySeq qn cvmod
    -> { A : positive | forall n:nat, Qlt (Qabs (qn n)) (Z.pos A # 1) }.

Lemma CReal_mult_cauchy
  : forall (xn yn zn : nat -> Q) (Ay Az : positive) (cvmod : positive -> nat),
    QSeqEquiv xn yn cvmod
    -> QCauchySeq zn Pos.to_nat
    -> (forall n:nat, Qlt (Qabs (yn n)) (Z.pos Ay # 1))
    -> (forall n:nat, Qlt (Qabs (zn n)) (Z.pos Az # 1))
    -> QSeqEquiv (fun n:nat => xn n * zn n) (fun n:nat => yn n * zn n)
                (fun p => max (cvmod (2 * (Pos.max Ay Az) * p)%positive)
                           (Pos.to_nat (2 * (Pos.max Ay Az) * p)%positive)).

Lemma linear_max : forall (p Ax Ay : positive) (i : nat),
  le (Pos.to_nat p) i
  -> (Init.Nat.max (Pos.to_nat (2 * Pos.max Ax Ay * p))
                 (Pos.to_nat (2 * Pos.max Ax Ay * p)) <= Pos.to_nat (2 * Pos.max Ax Ay) * i)%nat.

Definition CReal_mult (x y : CReal) : CReal.

Infix "*" := CReal_mult : CReal_scope.

Lemma CReal_mult_unfold : forall x y : CReal,
    QSeqEquivEx (proj1_sig (CReal_mult x y))
                (fun n : nat => proj1_sig x n * proj1_sig y n)%Q.

Lemma CReal_mult_assoc_bounded_r : forall (xn yn zn : nat -> Q),
    QSeqEquivEx xn yn
    -> QSeqEquiv zn zn Pos.to_nat
    -> QSeqEquivEx (fun n => xn n * zn n)%Q (fun n => yn n * zn n)%Q.

Lemma CReal_mult_assoc : forall x y z : CReal,
    CRealEq (CReal_mult (CReal_mult x y) z)
            (CReal_mult x (CReal_mult y z)).

Lemma CReal_mult_comm : forall x y : CReal,
    CRealEq (CReal_mult x y) (CReal_mult y x).

Lemma CReal_mult_proper_l : forall x y z : CReal,
    CRealEq y z -> CRealEq (CReal_mult x y) (CReal_mult x z).

Lemma CReal_mult_lt_0_compat : forall x y : CReal,
    CRealLt (inject_Q 0) x
    -> CRealLt (inject_Q 0) y
    -> CRealLt (inject_Q 0) (CReal_mult x y).

Lemma CReal_mult_plus_distr_l : forall r1 r2 r3 : CReal,
    r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).

Lemma CReal_mult_plus_distr_r : forall r1 r2 r3 : CReal,
    (r2 + r3) * r1 == (r2 * r1) + (r3 * r1).

Lemma CReal_mult_1_l : forall r: CReal, 1 * r == r.

Lemma CReal_isRingExt : ring_eq_ext CReal_plus CReal_mult CReal_opp CRealEq.

Lemma CReal_isRing : ring_theory (inject_Q 0) (inject_Q 1)
                                 CReal_plus CReal_mult
                                 CReal_minus CReal_opp
                                 CRealEq.

Add Parametric Morphism : CReal_mult
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_mult_morph.

Instance CReal_mult_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_mult.

Add Parametric Morphism : CReal_opp
    with signature CRealEq ==> CRealEq
      as CReal_opp_morph.

Instance CReal_opp_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq CRealEq) CReal_opp.

Add Parametric Morphism : CReal_minus
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_minus_morph.

Instance CReal_minus_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_minus.

Add Ring CRealRing : CReal_isRing.

Lemma CReal_opp_0 : -0 == 0.

Lemma CReal_opp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2.

Lemma CReal_opp_involutive : forall x:CReal, --x == x.

Lemma CReal_opp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.

Lemma CReal_mult_0_l : forall r, 0 * r == 0.

Lemma CReal_mult_0_r : forall r, r * 0 == 0.

Lemma CReal_mult_1_r : forall r, r * 1 == r.

Lemma CReal_opp_mult_distr_l
  : forall r1 r2 : CReal, CRealEq (CReal_opp (CReal_mult r1 r2))
                              (CReal_mult (CReal_opp r1) r2).

Lemma CReal_mult_lt_compat_l : forall x y z : CReal,
    0 < x -> y < z -> x*y < x*z.

Lemma CReal_mult_lt_compat_r : forall x y z : CReal,
    0 < x -> y < z -> y*x < z*x.

Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal),
    r # 0
    -> CRealEq (CReal_mult r r1) (CReal_mult r r2)
    -> CRealEq r1 r2.

Field

Fixpoint INR (n:nat) : CReal :=
  match n with
  | O => 0
  | S O => 1
  | S n => INR n + 1
  end.

Fixpoint IPR_2 (p:positive) : CReal :=
  match p with
  | xH => 1 + 1
  | xO p => IPR_2 p + IPR_2 p
  | xI p => (1 + IPR_2 p) + (1 + IPR_2 p)
  end.

Definition IPR (p:positive) : CReal :=
  match p with
  | xH => 1
  | xO p => IPR_2 p
  | xI p => 1 + IPR_2 p
  end.

Definition IZR (z:Z) : CReal :=
  match z with
  | Z0 => 0
  | Zpos n => IPR n
  | Zneg n => - IPR n
  end.

Notation "2" := (IZR 2) : CReal_scope.

Lemma S_INR : forall n:nat, INR (S n) == INR n + 1.

Lemma le_succ_r_T : forall n m : nat, (n <= S m)%nat -> {(n <= m)%nat} + {n = S m}.

Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.

Lemma S_O_plus_INR : forall n:nat, INR (1 + n) == INR 1 + INR n.

Lemma plus_INR : forall n m:nat, INR (n + m) == INR n + INR m.

Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) == INR n - INR m.

Lemma mult_INR : forall n m:nat, INR (n * m) == INR n * INR m.

Lemma IZN : forall n:Z, (0 <= n)%Z -> { m : nat | n = Z.of_nat m }.

Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p.

Lemma FinjectP2_CReal : forall (p:positive) (k:nat),
    (proj1_sig (IPR_2 p) k == Z.pos p~0 # 1)%Q.

Lemma FinjectP_CReal : forall (p:positive) (k:nat),
    (proj1_sig (IPR p) k == Z.pos p # 1)%Q.

Lemma IPR_pos : forall p:positive, 0 < IPR p.

Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p.

Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n).

Lemma plus_IZR_NEG_POS :
  forall p q:positive, IZR (Zpos p + Zneg q) == IZR (Zpos p) + IZR (Zneg q).

Lemma plus_IPR : forall n m:positive, IPR (n + m) == IPR n + IPR m.

Lemma plus_IZR : forall n m:Z, IZR (n + m) == IZR n + IZR m.

Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m.

Lemma mult_IZR : forall n m:Z, IZR (n * m) == IZR n * IZR m.

Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n.

Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m.

Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.

Lemma Z_R_minus : forall n m:Z, IZR n - IZR m == IZR (n - m).

Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.

Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.

Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.

Lemma CReal_iterate_one : forall (n : nat),
    IZR (Z.of_nat n) == inject_Q (Z.of_nat n # 1).

Lemma FinjectZ_CReal : forall z : Z,
    IZR z == inject_Q (z # 1).

Lemma Rarchimedean
  : forall x:CReal,
    { n:Z & x < IZR n < x+2 }.

Lemma CRealLtDisjunctEpsilon : forall a b c d : CReal,
    (CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b + CRealLt c d.

Lemma CRealShiftReal : forall (x : CReal) (k : nat),
    QCauchySeq (fun n => proj1_sig x (plus n k)) Pos.to_nat.

Lemma CRealShiftEqual : forall (x : CReal) (k : nat),
    CRealEq x (exist _ (fun n => proj1_sig x (plus n k)) (CRealShiftReal x k)).

Definition CRealNegShift (x : CReal)
  : CRealLt x (inject_Q 0)
    -> { y : prod positive CReal | CRealEq x (snd y)
                                   /\ forall n:nat, Qlt (proj1_sig (snd y) n) (-1 # fst y) }.

Definition CRealPosShift (x : CReal)
  : CRealLt (inject_Q 0) x
    -> { y : prod positive CReal | CRealEq x (snd y)
                                   /\ forall n:nat, Qlt (1 # fst y) (proj1_sig (snd y) n) }.

Lemma CReal_inv_neg : forall (yn : nat -> Q) (k : positive),
    (QCauchySeq yn Pos.to_nat)
    -> (forall n : nat, yn n < -1 # k)%Q
    -> QCauchySeq (fun n : nat => / yn (Pos.to_nat k ^ 2 * n)%nat) Pos.to_nat.

Lemma CReal_inv_pos : forall (yn : nat -> Q) (k : positive),
    (QCauchySeq yn Pos.to_nat)
    -> (forall n : nat, 1 # k < yn n)%Q
    -> QCauchySeq (fun n : nat => / yn (Pos.to_nat k ^ 2 * n)%nat) Pos.to_nat.

Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal.

Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : CReal_scope.

Lemma CReal_inv_0_lt_compat
  : forall (r : CReal) (rnz : r # 0),
    0 < r -> 0 < ((/ r) rnz).

Lemma CReal_linear_shift : forall (x : CReal) (k : nat),
    le 1 k -> QCauchySeq (fun n => proj1_sig x (k * n)%nat) Pos.to_nat.

Lemma CReal_linear_shift_eq : forall (x : CReal) (k : nat) (kPos : le 1 k),
    CRealEq x
    (exist (fun n : nat -> Q => QCauchySeq n Pos.to_nat)
           (fun n : nat => proj1_sig x (k * n)%nat) (CReal_linear_shift x k kPos)).

Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0),
        ((/ r) rnz) * r == 1.

Lemma CReal_inv_r : forall (r:CReal) (rnz : r # 0),
        r * ((/ r) rnz) == 1.

Lemma CReal_inv_1 : forall nz : 1 # 0, (/ 1) nz == 1.

Lemma CReal_inv_mult_distr :
  forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0),
    (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.

Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0),
    x == y
    -> (/ x) rxnz == (/ y) rynz.

Lemma CReal_mult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.

Lemma CReal_mult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2.

Lemma CReal_mult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2.

Lemma CReal_mult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2.

Lemma CReal_mult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r.

Fixpoint pow (r:CReal) (n:nat) : CReal :=
  match n with
    | O => 1
    | S n => r * (pow r n)
  end.

Definition IQR (q:Q) : CReal :=
  match q with
  | Qmake a b => IZR a * (CReal_inv (IPR b)) (inr (IPR_pos b))
  end.

Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m.

Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m.

Lemma IQR_pos : forall q:Q, Qlt 0 q -> 0 < IQR q.

Lemma opp_IQR : forall q:Q, IQR (- q) == - IQR q.

Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q.

Lemma CReal_mult_le_compat_l_half : forall r r1 r2,
    0 < r -> r1 <= r2 -> r * r1 <= r * r2.

Lemma IQR_lt : forall n m:Q, Qlt n m -> IQR n < IQR m.

Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q).

Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m.

Add Parametric Morphism : IQR
    with signature Qeq ==> CRealEq
      as IQR_morph.

Instance IQR_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful Qeq CRealEq) IQR.

Lemma CReal_invQ : forall (b : positive) (pos : Qlt 0 (Z.pos b # 1)),
    CRealEq (CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos)))
            (inject_Q (1 # b)).

Lemma FinjectQ_CReal : forall q : Q,
    IQR q == inject_Q q.

Lemma CReal_gen_inject : forall (n : nat),
    gen_phiZ (inject_Q 0) (inject_Q 1) CReal_plus CReal_mult CReal_opp
             (Z.of_nat n)
    == inject_Q (Z.of_nat n # 1).

Lemma CRealArchimedean
  : forall x:CReal, { n:Z & CRealLt x (gen_phiZ (inject_Q 0) (inject_Q 1) CReal_plus
                                                CReal_mult CReal_opp n) }.

Close Scope CReal_scope.

Close Scope Q.