fact: Definition CRPartialOrder : PartialOrder := makePartialOrder (@msp_eq CR) CRle CRmonotone CRantitone CRle_antisym CRle_refl CRle_trans (Default.monotone_def _) (Default.antitone_def _).
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRGroupOps CoRN.order.PartialOrder