Addition

Lifting addition over Q by one parameter yields a rational translation function.
Lemma Qtranslate_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:QS => (a[+]b):QS) Qpos2QposInf.

Definition Qtranslate_uc (a:Q_as_MetricSpace) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (Qtranslate_uc_prf a).

Definition translate (a:Q) : CR --> CR := Cmap QPrelengthSpace (Qtranslate_uc a).

Lemma translate_ident : forall x:CR, (translate 0 x==x)%CR.

Lifting translate yields binary addition over CR.
Lemma Qplus_uc_prf : is_UniformlyContinuousFunction Qtranslate_uc Qpos2QposInf.

Definition Qplus_uc : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qplus_uc_prf.

Definition CRplus : CR --> CR --> CR := Cmap2 QPrelengthSpace QPrelengthSpace Qplus_uc.

Notation "x + y" := (ucFun2 CRplus x y) : CR_scope.

Lemma CRplus_translate : forall (a:Q) (y:CR), (' a + y == translate a y)%CR.


Lemma translate_Qplus : forall a b:Q, (translate a ('b)=='(a+b)%Q)%CR.

Negation

Lifting negation on Q yields negation on CR.
Lemma Qopp_uc_prf : is_UniformlyContinuousFunction Qopp Qpos2QposInf.

Definition Qopp_uc : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qopp_uc_prf.

Definition CRopp : CR -> CR := Cmap QPrelengthSpace Qopp_uc.

Notation "- x" := (CRopp x) : CR_scope.

Subtraction

There is no subtraction on CR. It is simply notation for adding a negated quantity. This way all lemmas about addition automatically apply to subtraction.
Notation "x - y" := (x + (- y))%CR : CR_scope.

Inequality

First a predicate for nonnegative numbers is defined.
Definition CRnonNeg (x:CR) := forall e:Qpos, (-e) <= (approximate x e).
And similarly for nonpositive.
Definition CRnonPos (x:CR) := forall e:Qpos, (approximate x e) <= e.
Inequality is defined in terms of nonnegativity.
Definition CRle (x y:CR) := (CRnonNeg (y - x))%CR.

Infix "<=" := CRle : CR_scope.
Basic properties of inequality
Lemma CRle_refl : forall x, (x <= x)%CR.

Lemma CRle_def : forall x y, (x==y <-> (x <= y /\ y <= x))%CR.

Lemma CRle_trans : forall x y z, (x <= y -> y <= z -> x <= z)%CR.

Maximum

QboundBelow ensures that a real number is at least some fixed rational number. It is the lifting of the first parameter of Qmax.
Lemma QboundBelow_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:QS => (Qmax a b):QS) Qpos2QposInf.

Definition QboundBelow_uc (a:Q_as_MetricSpace) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (QboundBelow_uc_prf a).

Definition boundBelow (a:Q) : CR --> CR := Cmap QPrelengthSpace (QboundBelow_uc a).

CRmax is the lifting of QboundBelow.
Lemma Qmax_uc_prf : is_UniformlyContinuousFunction QboundBelow_uc Qpos2QposInf.

Definition Qmax_uc : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qmax_uc_prf.

Definition CRmax : CR --> CR --> CR := Cmap2 QPrelengthSpace QPrelengthSpace Qmax_uc.

Lemma CRmax_boundBelow : forall (a:Q) (y:CR), (CRmax (' a) y == boundBelow a y)%CR.
Basic properties of CRmax.
Lemma CRmax_ub_l : forall x y, (x <= CRmax x y)%CR.

Lemma CRmax_ub_r : forall x y, (y <= CRmax x y)%CR.

Lemma CRmax_lub: forall x y z : CR, (x <= z -> y <= z -> CRmax x y <= z)%CR.

Minimum

QboundAbove ensures that a real number is at most some fixed rational number. It is the lifting of the first parameter of Qmin.
Lemma QboundAbove_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:QS => (Qmin a b):QS) Qpos2QposInf.

Definition QboundAbove_uc (a:Q_as_MetricSpace) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (QboundAbove_uc_prf a).

Definition boundAbove (a:Q) : CR --> CR := Cmap QPrelengthSpace (QboundAbove_uc a).

CRmin is the lifting of QboundAbove.
Lemma Qmin_uc_prf : is_UniformlyContinuousFunction QboundAbove_uc Qpos2QposInf.

Definition Qmin_uc : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qmin_uc_prf.

Definition CRmin : CR --> CR --> CR := Cmap2 QPrelengthSpace QPrelengthSpace Qmin_uc.

Lemma CRmin_boundAbove : forall (a:Q) (y:CR), (CRmin (' a) y == boundAbove a y)%CR.

Basic properties of CRmin.
Lemma CRmin_lb_l : forall x y, (CRmin x y <= x)%CR.

Lemma CRmin_lb_r : forall x y, (CRmin x y <= y)%CR.

Lemma CRmin_glb: forall x y z : CR, (z <= x -> z <= y -> z <= CRmin x y)%CR.