proposition: Lemma Cap_correct : forall X Y plX, msp_eq (Cap Y plX) (Cap_slow X Y).
proof: Proof. intros. split. apply Qle_refl. intro f. split. apply Qle_refl. apply (Cap_fun_correct plX f). 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