proposition: Lemma Cmap_strong_correct : forall X Y plX, msp_eq (@Cmap_strong X Y plX) (@Cmap_strong_slow X Y).
proof: Proof. intros X Y plX. split. apply Qle_refl. intro f. destruct (Cmap_correct plX f) as [_ H0]. split. apply Qle_refl. intro x. apply H0. 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