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