fact: Definition Zminus_max_min_antidistr_r : forall x y z : Z, x - Z.max y z = Z.min (x-y) (x-z) := fun a => @antitone_join_meet_distr Zto _ (Zminus_antitone a).
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder