fact: Definition Zmin_max_de_morgan : forall x y : Z, -(Z.min x y) = Z.max (-x) (-y) := @antitone_meet_join_distr Zto _ Zopp_le_compat.
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder