fact: Definition Zmax_plus_distr_r : forall x y z : Z, x + Z.max y z = Z.max (x+y) (x+z) := fun a => @monotone_join_distr Zto _ (Zplus_monotone_r a).
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder