proposition: Lemma Cmap_correct : msp_eq Cmap (Cmap_slow f).
proof: Proof. apply ucEq_equiv. intros x e1 e2. simpl. unfold Cmap_slow_raw. rewrite Qplus_0_r. apply (@mu_sum X plX Y e2 (e1::nil)). simpl. destruct (mu f e1) as [d1|]; try constructor. destruct (mu f e2) as [d2|]; try constructor. simpl. eapply ball_weak_le;[|apply regFun_prf]. simpl. apply Qplus_le_r. rewrite <- (Qmult_1_l (proj1_sig d2)), Qmult_assoc. apply Qmult_le_r. apply Qpos_ispos. discriminate. 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