ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index d976b01c6..2807532ca 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1118,6 +1118,21 @@ Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 
 (**********************************************************************)
+(** * Minimum and maximum *)
+
+Unboxed Definition Zmax (n m:Z) :=
+  match n ?= m with
+    | Eq | Gt => n
+    | Lt => m
+  end.
+
+Unboxed Definition Zmin (n m:Z) :=
+  match n ?= m with
+    | Eq | Lt => n
+    | Gt => m
+  end.
+
+(**********************************************************************)
 (** * Absolute value on integers *)
 
 Definition Zabs_nat (x:Z) : nat :=