proposition: Lemma distmapret: forall (X:MetricSpace), ucEq (uc_compose dist (@Map_uc _ _ (@Cunit X))) (@Cunit (StepFSup X)).
proof: Proof. intros X x e1 e2. rewrite Qplus_0_r. simpl. unfold dist_raw. unfold StepFSupBall. assert (@StepF_eq (msp_as_RSetoid X) (Map (fun z : Complete X => approximate z e1) (Map (Cunit_fun X) x)) (Map (fun z => (approximate ((Cunit_fun X) z) e1)) x)). { apply StepF_Qeq_eq; rewrite <- Map_compose_Map; reflexivity. } rewrite H. clear H. simpl. rewrite (Map_identity _ x). set (b:=(@ballS X (proj1_sig e1+proj1_sig e2))). set (f:=(@join _ _) ^@> (constStepF b)). cut (StepFfoldProp (f <@> x )). unfold f; evalStepF; tauto. apply: StepFfoldPropForall_Map. simpl. intro a. apply ball_refl. apply (Qpos_nonneg (e1+e2)). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionMonad CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.metric2.Complete CoRN.model.metric2.LinfMetricMonad CoRN.metric2.StepFunctionSetoid CoRN.tactics.Qauto