NBinary improved, contains more, subsumes NOrderedType

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

1 files changed, 17 insertions, 1 deletions

diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 53ba50ffe..3a87880ac 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -14,5 +14,21 @@ Require Export BinPos.
 Require Export BinNat.
 Require Export Nnat.
 Require Export Ndigits.
-
 Require Export NArithRing.
+Require NBinary Nminmax.
+
+Module N := NBinary.N <+ Nminmax.Nextend.
+
+(** [N] contains An [order] tactic for natural numbers *)
+
+(** Note that [N.order] is domain-agnostic: it will not prove
+    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
+
+Local Open Scope N_scope.
+
+Section TestOrder.
+ Let test : forall x y, x<=y -> y<=x -> x=y.
+ Proof.
+ N.order.
+ Qed.
+End TestOrder.