Require Export ZArith_base.
Require Import ClassicalDedekindReals.
Require Import ConstructiveCauchyReals.
Require Import ConstructiveCauchyRealsMult.
Require Import ConstructiveRcomplete.
Require Import ConstructiveLUB.
Require Export Rdefinitions.
Local Open Scope R_scope.

Open Scope CReal_scope.

Lemma Rrepr_0 : Rrepr 0 == 0.

Lemma Rrepr_1 : Rrepr 1 == 1.

Lemma Rrepr_plus : forall x y:R, Rrepr (x + y) == Rrepr x + Rrepr y.

Lemma Rrepr_opp : forall x:R, Rrepr (- x) == - Rrepr x.

Lemma Rrepr_minus : forall x y:R, Rrepr (x - y) == Rrepr x - Rrepr y.

Lemma Rrepr_mult : forall x y:R, Rrepr (x * y) == Rrepr x * Rrepr y.

Lemma Rrepr_inv : forall (x:R) (xnz : Rrepr x # 0),
    Rrepr (/ x) == (/ Rrepr x) xnz.

Lemma Rrepr_le : forall x y:R, (x <= y)%R <-> Rrepr x <= Rrepr y.

Lemma Rrepr_appart : forall x y:R,
    (x <> y)%R -> Rrepr x # Rrepr y.

Lemma Rappart_repr : forall x y:R,
    Rrepr x # Rrepr y -> (x <> y)%R.

Close Scope CReal_scope.

Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
#[global]
Hint Resolve Rplus_comm: real.

Lemma Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
#[global]
Hint Resolve Rplus_assoc: real.

Lemma Rplus_opp_r : forall r:R, r + - r = 0.
#[global]
Hint Resolve Rplus_opp_r: real.

Lemma Rplus_0_l : forall r:R, 0 + r = r.
#[global]
Hint Resolve Rplus_0_l: real.

Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
#[global]
Hint Resolve Rmult_comm: real.

Lemma Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
#[global]
Hint Resolve Rmult_assoc: real.

Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
#[global]
Hint Resolve Rinv_l: real.

Lemma Rmult_1_l : forall r:R, 1 * r = r.
#[global]
Hint Resolve Rmult_1_l: real.

Lemma R1_neq_R0 : 1 <> 0.
#[global]
Hint Resolve R1_neq_R0: real.

Lemma
  Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
#[global]
Hint Resolve Rmult_plus_distr_l: real.

Lemma Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.

Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.

Lemma Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.

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

#[global]
Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.

Fixpoint INR (n:nat) : R :=
  match n with
  | O => 0
  | S O => 1
  | S n => INR n + 1
  end.
Arguments INR n%_nat.

Lemma Rrepr_INR : forall n : nat,
    CRealEq (Rrepr (INR n)) (inject_Z (Z.of_nat n)).

Lemma Rrepr_IPR2 : forall n : positive,
    CRealEq (Rrepr (IPR_2 n)) (inject_Z (Z.pos (n~0))).

Lemma Rrepr_IPR : forall n : positive,
    CRealEq (Rrepr (IPR n)) (inject_Z (Z.pos n)).

Lemma Rrepr_IZR : forall n : Z,
    CRealEq (Rrepr (IZR n)) (inject_Z n).

Lemma archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.

Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.

Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m.

Definition is_lub (E:R -> Prop) (m:R) :=
  is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).

Lemma completeness :
    forall E:R -> Prop,
      bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.