proposition: Lemma Zeq_le_def : forall x y, x = y <-> x <= y /\ y <= x.
proof: Proof. intros. split. intros H; rewrite H. firstorder using Z.le_refl. firstorder using Zle_antisym. Qed.
imports: Coq.ZArith.Zmin Coq.ZArith.Zmax Coq.ZArith.ZArith CoRN.order.TotalOrder