proposition: Lemma Zpred_monotone : Zmonotone Z.pred.
proof: Proof. unfold Zmonotone, Default.monotone. intros x y H. rewrite (Zsucc_pred x) in H. rewrite (Zsucc_pred y) in H. auto with zarith. Qed.
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder