fact: Definition DN_bind {A: Type}: DN A -> forall B, (A -> DN B) -> DN B := fun X Y Z P => X (fun a => Z a P).
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.Classes.Morphisms