fact: Definition Zpred_min_distr : forall x y : Z, Z.pred (Z.min x y) = Z.min (Z.pred x ) (Z.pred y) := @monotone_meet_distr Zto _ Zpred_monotone.
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder