fact: Definition CRle_min_r : forall x y : CR, y <= x <-> CRmin x y == y := @le_meet_r (sl CRlat).
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.partialorder.CRpartialorder CoRN.order.SemiLattice CoRN.order.Lattice