fact: Definition Zsucc_max_distr : forall x y : Z, Z.succ (Z.max x y) = Z.max (Z.succ x ) (Z.succ y) := @monotone_join_distr Zto _ Zsucc_monotone.
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder