Lemma Qabs_uc_prf : is_UniformlyContinuousFunction
 (Qabs:Q_as_MetricSpace -> Q_as_MetricSpace) Qpos2QposInf.


Definition Qabs_uc : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction Qabs_uc_prf.

Definition CRabs : CR --> CR := Cmap QPrelengthSpace Qabs_uc.

Lemma CRabs_correct : forall x,
 (IRasCR (AbsIR x) == CRabs (IRasCR x))%CR.

Lemma CRabs_AbsSmall : forall a b, (CRabs b[<=]a) <-> AbsSmall a b.

Lemma CRabs_pos : forall x:CR, ('0 <= x -> CRabs x == x)%CR.

Lemma CRabs_neg: forall x, (x <= '0 -> CRabs x == - x)%CR.