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