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, 12 insertions, 3 deletions

diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 7211112f26..d29bb32eb2 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -18,7 +18,8 @@ Local Open Scope N_scope.
 
 (** * Implementation of [NAxiomsSig] module type via [BinNat.N] *)
 
-Module NBinaryAxiomsMod <: NAxiomsSig.
+Module Type N
+ <: NAxiomsSig <: UsualOrderedTypeFull <: TotalOrder <: DecidableTypeFull.
 
 (** Bi-directional induction. *)
 
@@ -65,6 +66,10 @@ apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1.
 right; now apply Pcompare_Eq_eq. now left. exfalso; now apply H.
 Qed.
 
+Definition eqb_eq := Neqb_eq.
+
+Definition compare_spec := Ncompare_spec.
+
 Theorem min_l : forall n m, n <= m -> Nmin n m = n.
 Proof.
 unfold Nmin, Nle; intros n m H.
@@ -138,6 +143,9 @@ Qed.
 
 Definition t := N.
 Definition eq := @eq N.
+Definition eqb := Neqb.
+Definition compare := Ncompare.
+Definition eq_dec := N_eq_dec.
 Definition zero := N0.
 Definition succ := Nsucc.
 Definition pred := Npred.
@@ -149,9 +157,10 @@ Definition le := Nle.
 Definition min := Nmin.
 Definition max := Nmax.
 
-End NBinaryAxiomsMod.
+Include NPropFunct
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
-Module Export NBinaryPropMod := NPropFunct NBinaryAxiomsMod.
+End N.
 
 (*
 Require Import NDefOps.