fact: Definition CRmax_min_absorb_l_r : forall x y : CR, CRmax x (CRmin y x) == x := @join_meet_absorb_l_r CRlat.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.partialorder.CRpartialorder CoRN.order.SemiLattice CoRN.order.Lattice