fact: Definition CRmax_monotone_l : forall a : CR, CRmonotone (fun x => CRmax x a) := @join_monotone_l CRlat.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.partialorder.CRpartialorder CoRN.order.SemiLattice CoRN.order.Lattice