proposition: Lemma Zminus_antitone : forall a : Z, Zantitone (fun x => a - x).
proof: Proof. change (forall a x y : Z, x <= y -> a + - y <= a + - x). intros. apply Zplus_le_compat; firstorder using Z.le_refl, Zopp_le_compat. Qed.
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder