Strict Inequality

First we defined positivity. We define positivity to contain a positive rational witness of a lower bound on x. This seems the best way because this witness contains exactly the information needed for functions (such as inverse and logorithm) that have domains restricted to the positive reals.
Definition CRpos (x:CR) := sig (fun e:Qpos => ' e <= x)%CR.

Lemma CRpos_wd : forall x y, (x==y)%CR -> (CRpos x) -> (CRpos y).

This is a characterization closer to Bishop's definiton. If we replace 2*e with e, the theorem still holds, but it could be very expensive to call. We prefer to avoid that.
Lemma CRpos_char : forall (e:Qpos) (x:CR), 2*e <= (approximate x e) ->
 CRpos x.

Negative reals are defined similarly.
Definition CRneg (x:CR) := sig (fun e:Qpos => x <= ' (-e)%Q)%CR.

Lemma CRneg_wd : forall x y, (x==y)%CR -> (CRneg x) -> (CRneg y).

Lemma CRneg_char : forall (e:Qpos) (x:CR), (approximate x e) <= -(2)*e ->
 CRneg x.

Strict inequality is defined in terms of positivity.
Definition CRlt (x y:CR) := CRpos (y-x)%CR.

Infix "<" := CRlt : CR_scope.

Lemma CRlt_wd : forall x1 x2, (x1==x2 -> forall y1 y2, y1==y2 -> x1 < y1 -> x2 < y2)%CR.

Apartness

Definition CRapart (x y:CR) := (x < y or y < x)%CR.

Notation "x >< y" := (CRapart x y) (at level 70, no associativity) : CR_scope.

Lemma CRapart_wd : forall x1 x2, (x1==x2 -> forall y1 y2, y1==y2 -> x1><y1 -> x2><y2)%CR.

Multiplication

The modulus of continuity for multiplication by a constant.
Definition Qscale_modulus (a:Q) (e:Qpos) : Q+∞ :=
match a with
| 0 # _ => ∞
| (Zpos an) # ad => Qpos2QposInf ((ad # an) * e)
| (Zneg an) # ad => Qpos2QposInf ((ad # an) * e)
end.

Lemma Qscale_modulus_elim : forall (P:QposInf -> Type) (x:Q) (e:Qpos),
(x==0 -> P ∞)%Q ->
(forall y:Qpos, AbsSmall (e/y)%Q (x)%Q -> (P y)) ->
P (Qscale_modulus x e).


Lemma Qscale_uc_prf (a:Q) : is_UniformlyContinuousFunction (fun b:Q => a*b) (Qscale_modulus a).

Scaling by a constant is Qmult lifted on one parameter.
Definition Qscale_uc (a:Q_as_MetricSpace) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (Qscale_uc_prf a).

Definition scale (a:Q) : CR --> CR := Cmap QPrelengthSpace (Qscale_uc a).

CRboundAbs clamps a real number between -c and c where c is rational.
Definition QboundAbs (c:Qpos) := uc_compose (QboundBelow_uc (-c)) (QboundAbove_uc c).

Definition CRboundAbs (c:Qpos) := Cmap QPrelengthSpace (QboundAbs c).

Lemma QboundAbs_absorb: forall (a b:Qpos) (c:Q),
 a <= b ->
 QboundAbs b (QboundAbs a c) == QboundAbs a c.

Properties of CRboundAbs.
Lemma CRboundAbs_Eq : forall (a:Qpos) (x:CR),
 ('(-a)%Q <= x -> x <= ' a ->
 CRboundAbs a x == x)%CR.

Lemma QboundAbs_elim : forall (z:Qpos) (a:Q) (P:Q->Prop),
((z <= a)%Q -> P z) ->
((a <= -z)%Q -> P (- z)%Q) ->
(AbsSmall (z:Q) a -> P (a)) ->
P (QboundAbs z a).

The modulus of continuity for multiplication depends on the bound, c, on the second argument.
Definition Qmult_modulus (c:Qpos)(e:Qpos) : Q+∞ := (e / c)%Qpos.

Lemma Qmult_uc_prf (c:Qpos) : is_UniformlyContinuousFunction (fun a => uc_compose (Qscale_uc a) (QboundAbs c)) (Qmult_modulus c).
Definition Qmult_uc (c:Qpos) : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace:=
Build_UniformlyContinuousFunction (Qmult_uc_prf c).

This multiply should be used when a bound on the absolute value of the second argument is known.
Definition CRmult_bounded (c:Qpos) : CR --> CR --> CR :=
Cmap2 QPrelengthSpace QPrelengthSpace (Qmult_uc c).

CR_b computes a rational bound on the absolute value of x
Definition CR_b (e:Qpos) (x:CR) : Q+.
Defined.

Lemma CR_b_lowerBound : forall e x, (' (-CR_b e x)%Q <= x)%CR.

Lemma CR_b_upperBound : forall e x, (x <= 'CR_b e x)%CR.

This version of multiply computes a bound on the second argument just in time. It should be avoided in favour of the bounded version whenever possible.
Definition CRmult x y := ucFun2 (CRmult_bounded (CR_b (1#1) y)) x y.

Infix "*" := CRmult : CR_scope.

Lemma CRmult_bounded_weaken : forall (c1 c2:Qpos) x y,
((' (-c1)%Q <= y) -> (y <= ' c1) -> (c1 <= c2)%Q ->
CRmult_bounded c1 x y == CRmult_bounded c2 x y)%CR.

Lemma CRmult_bounded_mult : forall (c:Qpos) (x y:CR),
 (' (-c)%Q <= y -> y <= ' c ->
  CRmult_bounded c x y == x*y)%CR.
Lemma CRmult_scale : forall (a:Q) (y:CR), ((' a)*y==scale a y)%CR.
Lemma scale_Qmult : forall a b:Q, (scale a ('b)=='(a*b)%Q)%CR.

Inverse

The modulus of continuity for inverse depends on a rational bound away from 0 of x.
Definition Qinv_modulus (c:Qpos) (e:Qpos) : Q+ := (c*c*e)%Qpos.

Lemma Qpos_Qmax : forall (a:Qpos) (b:Q), 0<Qmax a b.

Lemma Qinv_pos_uc_prf (c:Qpos) : is_UniformlyContinuousFunction (fun a:Q => /(Qmax c a) ) (Qinv_modulus c).


Definition Qinv_pos_uc (c:Qpos) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (Qinv_pos_uc_prf c).

Lemma Qinv_pos_uc_wd : forall (c1 c2:Qpos), (c1 <= c2) -> forall x, (c2 <= x) -> st_eq (Qinv_pos_uc c1 x) (Qinv_pos_uc c2 x).

CRinv_pos works for inputs greater than c
Definition CRinv_pos (c:Qpos) : CR --> CR := (Cmap QPrelengthSpace (Qinv_pos_uc c)).

Lemma CRinv_pos_weaken : forall (c1 c2:Qpos), c1 <= c2 -> forall (x:CR), (' c2 <= x -> CRinv_pos c1 x == CRinv_pos c2 x)%CR.

Lemma CRinv_pos_Qinv : forall (c:Qpos) x, (c <= x)%Q -> (CRinv_pos c (' x) == (' (/x)))%CR.

CRinv works for inputs apart from 0
Definition CRinv (x:CR)(x_: (x >< ' 0)%CR) : CR.
Defined.


Lemma CRinv_pos_inv : forall (c:Qpos) (x:CR) x_,
 (inject_Q c <= x ->
  CRinv_pos c x == CRinv x x_)%CR.

Lemma CRinv_wd : forall (x y:CR) x_ y_, (x == y -> CRinv x x_ == CRinv y y_)%CR.

Lemma CRinv_irrelvent : forall x x_ x__, (CRinv x x_ == CRinv x x__)%CR.