proposition: Lemma ARtoCR_preserves_abs : forall x : AR, cast AR CR (ARabs x) = CRabs (cast AR CR x).
proof: Proof. intro x. unfold cast, ARtoCR, ARtoCR_uc. unfold MetricMorphisms.Eembed. unfold ARabs, CRabs. rewrite <- (fast_MonadLaw2 AQPrelengthSpace (MetricMorphisms.EPrelengthSpace QPrelengthSpace (cast AQ Q_as_MetricSpace)) (MetricMorphisms.metric_embed_uc (cast AQ Q_as_MetricSpace)) AQabs_uc). rewrite <- (fast_MonadLaw2 (MetricMorphisms.EPrelengthSpace QPrelengthSpace (cast AQ Q_as_MetricSpace)) QPrelengthSpace Qabs_uc (MetricMorphisms.metric_embed_uc (cast AQ Q_as_MetricSpace)) x). apply Cmap_wd. 2: reflexivity. apply ucEq_equiv. intro d. simpl. apply Qball_0, aq_abs. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRabs CoRN.reals.faster.ARArith