proposition: Lemma Cmap_prf : is_UniformlyContinuousFunction Cmap_fun (mu f).
proof: Proof. intros e0 x y Hxy e1 e2. simpl. rewrite <- Qplus_assoc. apply (@mu_sum X plX Y e2 (e1::e0::nil)). simpl. destruct (mu f e1) as [d1|];[|constructor]. destruct (mu f e0) as [d0|];[|constructor]. destruct (mu f e2) as [d2|];[|constructor]. simpl in *. rewrite Qplus_assoc. apply Hxy. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.List CoRN.stdlib_omissions.Q