fact: Definition CRmax_le_compat : forall w x y z : CR, w<=y -> x<=z -> CRmax w x <= CRmax y z := @join_le_compat CRlat.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.partialorder.CRpartialorder CoRN.order.SemiLattice CoRN.order.Lattice