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