proposition: Lemma CRboundAbs_Eq : forall (a:Qpos) (x:CR), ('(-proj1_sig a)%Q <= x -> x <= ' proj1_sig a -> CRboundAbs a x == x)%CR.
proof: Proof. intros a x Ha Hb. unfold CRboundAbs. transitivity (uc_compose (Cmap QPrelengthSpace (QboundBelow_uc (-proj1_sig a))) (Cmap QPrelengthSpace (QboundAbove_uc (proj1_sig a))) x). simpl (Cmap QPrelengthSpace (QboundAbs a) x). simpl ((Cmap QPrelengthSpace (QboundBelow_uc (- ` a)) ∘ Cmap QPrelengthSpace (QboundAbove_uc (` a))) x). repeat rewrite -> Cmap_fun_correct. apply MonadLaw2. simpl ((Cmap QPrelengthSpace (QboundBelow_uc (- ` a)) ∘ Cmap QPrelengthSpace (QboundAbove_uc (` a))) x). change (boundBelow (-proj1_sig a) (boundAbove (proj1_sig a) x) == x)%CR. assert (X:(boundAbove (proj1_sig a) x==x)%CR). rewrite <- CRmin_boundAbove. rewrite <- CRle_min_r. assumption. rewrite -> X. rewrite <- CRmax_boundBelow. rewrite <- CRle_max_r. assumption. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names