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