Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natural numbers are isomorphic. Added NatScope and IntScope for abstract developments.

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

14 files changed, 140 insertions, 944 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 444175c14..2a17754d5 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -1,33 +1,52 @@
-Require Export NumPrelude.
 Require Export NZAxioms.
 
 Set Implicit Arguments.
 
 Module Type NAxiomsSig.
 Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
-Open Local Scope NatIntScope.
 
-Notation N := NZ (only parsing).
-Notation E := NZE (only parsing).
+Delimit Scope NatScope with Nat.
+Notation N := NZ.
+Notation Neq := NZeq.
+Notation N0 := NZ0.
+Notation N1 := (NZsucc NZ0).
+Notation S := NZsucc.
+Notation P := NZpred.
+Notation plus := NZplus.
+Notation times := NZtimes.
+Notation minus := NZminus.
+Notation "x == y"  := (NZeq x y) (at level 70) : NatScope.
+Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatScope.
+Notation "0" := NZ0 : NatScope.
+Notation "1" := (NZsucc NZ0) : NatScope.
+Notation "x + y" := (NZplus x y) : NatScope.
+Notation "x - y" := (NZminus x y) : NatScope.
+Notation "x * y" := (NZtimes x y) : NatScope.
+Notation "x < y" := (NZlt x y) : NatScope.
+Notation "x <= y" := (NZle x y) : NatScope.
+Notation "x > y" := (NZlt y x) (only parsing) : NatScope.
+Notation "x >= y" := (NZle y x) (only parsing) : NatScope.
+
+Open Local Scope NatScope.
 
 Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A.
 Implicit Arguments recursion [A].
 
 Axiom pred_0 : P 0 == 0.
 
-Axiom recursion_wd : forall (A : Set) (EA : relation A),
-  forall a a' : A, EA a a' ->
-    forall f f' : N -> A -> A, eq_fun2 E EA EA f f' ->
+Axiom recursion_wd : forall (A : Set) (Aeq : relation A),
+  forall a a' : A, Aeq a a' ->
+    forall f f' : N -> A -> A, eq_fun2 Neq Aeq Aeq f f' ->
       forall x x' : N, x == x' ->
-        EA (recursion a f x) (recursion a' f' x').
+        Aeq (recursion a f x) (recursion a' f' x').
 
 Axiom recursion_0 :
   forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
 
 Axiom recursion_succ :
-  forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
-    EA a a -> fun2_wd E EA EA f ->
-      forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
+  forall (A : Set) (Aeq : relation A) (a : A) (f : N -> A -> A),
+    Aeq a a -> fun2_wd Neq Aeq Aeq f ->
+      forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
 End NAxiomsSig.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 9705d05ba..c0c479dc8 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -1,8 +1,9 @@
 Require Export NAxioms.
 Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *)
 
-Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig).
-Open Local Scope NatIntScope.
+Module NBasePropFunct (Export NAxiomsMod : NAxiomsSig).
+
+Open Local Scope NatScope.
 
 (* We call the last property functor on NZ, which includes all the previous
 ones, to get all properties of NZ at once. This way we will include them
@@ -16,8 +17,14 @@ since unfolding is done only inside a functor. In fact, we'll do it in the
 files that prove the corresponding properties. In those files, we will also
 rename properties proved in NZ files by removing NZ from their names. In
 this way, one only has to consult, for example, NPlus.v to see all
-available properties for plus (i.e., one does not have to go to NAxioms.v
-and NZPlus.v). *)
+available properties for plus, i.e., one does not have to go to NAxioms.v
+for axioms and NZPlus.v for theorems. *)
+
+Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2.
+Proof NZsucc_wd.
+
+Theorem pred_wd : forall n1 n2 : N, n1 == n2 -> P n1 == P n2.
+Proof NZpred_wd.
 
 Theorem pred_succ : forall n : N, P (S n) == n.
 Proof NZpred_succ.
@@ -49,9 +56,9 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism if_zero with signature @eq ==> @eq ==> E ==> @eq as if_zero_wd.
+Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd.
 Proof.
-intros; unfold if_zero. apply recursion_wd with (EA := (@eq A)).
+intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold eq_fun2; now intros. assumption.
 Qed.
 
@@ -92,7 +99,7 @@ symmetry in H; false_hyp H neq_succ_0.
 Qed.
 
 Theorem induction :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
 Proof.
 intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption.
@@ -109,7 +116,7 @@ from N. *)
 Ltac induct n := induction_maker n ltac:(apply induction).
 
 Theorem case_analysis :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
 Proof.
 intros; apply induction; auto.
@@ -167,9 +174,9 @@ Fibonacci numbers *)
 Section PairInduction.
 
 Variable A : N -> Prop.
-Hypothesis A_wd : predicate_wd E A.
+Hypothesis A_wd : predicate_wd Neq A.
 
-Add Morphism A with signature E ==> iff as A_morph.
+Add Morphism A with signature Neq ==> iff as A_morph.
 Proof.
 exact A_wd.
 Qed.
@@ -191,9 +198,9 @@ End PairInduction.
 Section TwoDimensionalInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd E E R.
+Hypothesis R_wd : rel_wd Neq Neq R.
 
-Add Morphism R with signature E ==> E ==> iff as R_morph.
+Add Morphism R with signature Neq ==> Neq ==> iff as R_morph.
 Proof.
 exact R_wd.
 Qed.
@@ -221,9 +228,9 @@ End TwoDimensionalInduction.
 Section DoubleInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd E E R.
+Hypothesis R_wd : rel_wd Neq Neq R.
 
-Add Morphism R with signature E ==> E ==> iff as R_morph1.
+Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1.
 Proof.
 exact R_wd.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NDepRec.v b/theories/Numbers/Natural/Abstract/NDepRec.v
deleted file mode 100644
index 648786854..000000000
--- a/theories/Numbers/Natural/Abstract/NDepRec.v
+++ /dev/null
@@ -1,72 +0,0 @@
-Require Export NTimes.
-
-(* Here we allow dependent recursion only for domains with Libniz
-equality. The reason is that, if the domain is A : nat -> Set, then (A
-n) must coincide with (A n') whenever n == n'. However, it is possible
-to try to use arbitrary domain and require that n == n' -> A n = A n'. *)
-
-Module Type NDepRecSignature.
-Declare Module Export NDomainModule : NDomainEqSignature.
-Declare Module Export NBaseMod : NBaseSig with
-  Module NDomainModule := NDomainModule.
-(* Instead of these two lines, I would like to say
-Declare Module Export Nat : NBaseSig with Module NDomain : NatEqDomain. *)
-Open Local Scope NatScope.
-
-Parameter Inline dep_recursion :
-  forall A : N -> Set, A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.
-
-Axiom dep_recursion_0 :
-  forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)),
-    dep_recursion A a f 0 = a.
-
-Axiom dep_recursion_succ :
-  forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N),
-    dep_recursion A a f (S n) = f n (dep_recursion A a f n).
-
-End NDepRecSignature.
-
-Module NDepRecTimesProperties
-  (Import NDepRecModule : NDepRecSignature)
-  (Import NTimesMod : NTimesSig
-    with Module NPlusMod.NBaseMod := NDepRecModule.NBaseMod).
-Module Export NTimesPropertiesModule := NTimesPropFunct NTimesMod.
-Open Local Scope NatScope.
-
-Theorem not_0_implies_succ_dep : forall n, n # O -> {m : N | n == S m}.
-Proof.
-intro n; pattern n; apply dep_recursion; clear n;
-[intro H; now elim H | intros n _ _; now exists n].
-Qed.
-
-Theorem plus_eq_1_dep :
-  forall m n : N, m + n == 1 -> {m == 0 /\ n == 1} + {m == 1 /\ n == 0}.
-(* Why do we write == here instead of just = ? "x == y" is a notation
-for (E x y) declared (along with E := (@eq N)) in NatDomainEq signature. If we
-want to rewrite, e.g., plus_comm, which contains E, in a formula with
-=, setoid rewrite signals an error, because E is not declared a
-morphism w.r.t. = even though E is defined to be =. Thus, we need to
-use E instead of = in our formulas. *)
-Proof.
-intros m n; pattern m; apply dep_recursion; clear m.
-intro H.
-rewrite plus_0_l in H. left; now split.
-intros m IH H. rewrite plus_succ_l in H. apply succ_inj in H.
-apply plus_eq_0 in H. destruct H as [H1 H2].
-right; now split; [rewrite H1 |].
-Qed.
-
-Theorem times_eq_0_dep :
-  forall n m, n * m == 0 -> {n == 0} + {m == 0}.
-Proof.
-intros n m; pattern n; apply dep_recursion; pattern m; apply dep_recursion;
-clear n m.
-intros; left; reflexivity.
-intros; left; reflexivity.
-intros; right; reflexivity.
-intros n _ m _ H.
-rewrite times_succ_l in H. rewrite plus_succ_r in H; now apply succ_0 in H.
-Qed.
-
-End NDepRecTimesProperties.
-
diff --git a/theories/Numbers/Natural/Abstract/NDomain.v b/theories/Numbers/Natural/Abstract/NDomain.v
deleted file mode 100644
index 8f326ffec..000000000
--- a/theories/Numbers/Natural/Abstract/NDomain.v
+++ /dev/null
@@ -1,102 +0,0 @@
-Require Import Ring.
-Require Export NumPrelude.
-
-Module Type NDomainSignature.
-
-Parameter Inline N : Set.
-Parameter Inline E : N -> N -> Prop.
-Parameter Inline e : N -> N -> bool.
-
-(* Theoretically, we it is enough to have decidable equality e only.
-If necessary, E could be defined using a coercion. However, after we
-prove properties of natural numbers, we would like them to eventually
-use ordinary Leibniz equality. E.g., we would like the commutativity
-theorem, instantiated to nat, to say forall x y : nat, x + y = y + x,
-and not forall x y : nat, eq_true (e (x + y) (y + x))
-
-In fact, if we wanted to have decidable equality e only, we would have
-some trouble doing rewriting. If there is a hypothesis H : e x y, this
-means more precisely that H : eq_true (e x y). Such hypothesis is not
-recognized as equality by setoid rewrite because it does not have the
-form R x y where R is an identifier. *)
-
-Axiom E_equiv_e : forall x y : N, E x y <-> e x y.
-Axiom E_equiv : equiv N E.
-
-Add Relation N E
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
-
-Delimit Scope NatScope with Nat.
-Bind Scope NatScope with N.
-Notation "x == y" := (E x y) (at level 70) : NatScope.
-Notation "x # y" := (~ E x y) (at level 70) : NatScope.
-
-End NDomainSignature.
-
-(* Now we give NDomainSignature, but with E being Leibniz equality. If
-an implementation uses this signature, then more facts may be proved
-about it. *)
-Module Type NDomainEqSignature.
-
-Parameter Inline N : Set.
-Definition E := (@eq N).
-Parameter Inline e : N -> N -> bool.
-
-Axiom E_equiv_e : forall x y : N, E x y <-> e x y.
-Definition E_equiv : equiv N E := eq_equiv N.
-
-Add Relation N E
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
-
-Delimit Scope NatScope with Nat.
-Bind Scope NatScope with N.
-Notation "x == y" := (E x y) (at level 70) : NatScope.
-Notation "x # y" := ((E x y) -> False) (at level 70) : NatScope.
-(* Why do we need a new notation for Leibniz equality? See DepRec.v *)
-
-End NDomainEqSignature.
-
-Module NDomainProperties (Import NDomainModule : NDomainSignature).
-(* It also accepts module of type NatDomainEq *)
-Open Local Scope NatScope.
-
-Theorem Zneq_symm : forall n m, n # m -> m # n.
-Proof.
-intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
-Qed.
-
-(* The following easily follows from transitivity of e and E, but
-we need to deal with the coercion *)
-Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
-Proof.
-intros x x' Exx' y y' Eyy'.
-case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
-assert (x == y); [apply <- E_equiv_e; now rewrite H2 |
-assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
-rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]].
-assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 |
-assert (x == y); [rewrite Exx'; now rewrite Eyy' |
-rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
-Qed.
-
-Theorem NE_stepl : forall x y z : N, x == y -> x == z -> z == y.
-Proof.
-intros x y z H1 H2; now rewrite <- H1.
-Qed.
-
-Declare Left Step NE_stepl.
-
-(* The right step lemma is just transitivity of E *)
-Declare Right Step (proj1 (proj2 E_equiv)).
-
-Ltac stepl_ring t := stepl t; [| ring].
-Ltac stepr_ring t := stepr t; [| ring].
-
-End NDomainProperties.
-
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 66e028abe..b792beefe 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -1,49 +1,49 @@
-Require Export NAxioms.
+Require Import NBase.
 
-Module Homomorphism (Nat1 Nat2 : NBaseSig).
+Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
 
-Notation Local N1 := Nat1.NDomainModule.N.
-Notation Local N2 := Nat2.NDomainModule.N.
-Notation Local E1 := Nat1.NDomainModule.E.
-Notation Local E2 := Nat2.NDomainModule.E.
-Notation Local O1 := Nat1.O.
-Notation Local O2 := Nat2.O.
-Notation Local S1 := Nat1.S.
-Notation Local S2 := Nat2.S.
-Notation Local "x == y" := (Nat2.NDomainModule.E x y) (at level 70).
+Module NBasePropMod2 := NBasePropFunct NAxiomsMod2.
+
+Notation Local N1 := NAxiomsMod1.N.
+Notation Local N2 := NAxiomsMod2.N.
+Notation Local Eq1 := NAxiomsMod1.Neq.
+Notation Local Eq2 := NAxiomsMod2.Neq.
+Notation Local O1 := NAxiomsMod1.N0.
+Notation Local O2 := NAxiomsMod2.N0.
+Notation Local S1 := NAxiomsMod1.S.
+Notation Local S2 := NAxiomsMod2.S.
+Notation Local "n == m" := (Eq2 n m) (at level 70, no associativity).
 
 Definition homomorphism (f : N1 -> N2) : Prop :=
-  f O1 == O2 /\ forall x : N1, f (S1 x) == S2 (f x).
+  f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n).
 
 Definition natural_isomorphism : N1 -> N2 :=
-  Nat1.recursion O2 (fun (x : N1) (p : N2) => S2 p).
+  NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p).
 
-Add Morphism natural_isomorphism
-with signature E1 ==> E2
-as natural_isomorphism_wd.
+Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd.
 Proof.
 unfold natural_isomorphism.
-intros x y Exy.
-apply Nat1.recursion_wd with (EA := E2).
+intros n m Eqxy.
+apply NAxiomsMod1.recursion_wd with (Aeq := Eq2).
 reflexivity.
-unfold eq_fun2. intros _ _ _ y' y'' H. now apply Nat2.succ_wd.
+unfold eq_fun2. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
 assumption.
 Qed.
 
 Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2.
 Proof.
-unfold natural_isomorphism; now rewrite Nat1.recursion_0.
+unfold natural_isomorphism; now rewrite NAxiomsMod1.recursion_0.
 Qed.
 
 Theorem natural_isomorphism_succ :
-  forall x : N1, natural_isomorphism (S1 x) == S2 (natural_isomorphism x).
+  forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
 Proof.
-unfold natural_isomorphism;
-intro x; now rewrite (Nat1.recursion_succ Nat2.NDomainModule.E);
-[| unfold fun2_wd; intros; apply Nat2.succ_wd |].
+unfold natural_isomorphism.
+intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq);
+[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |].
 Qed.
 
-Theorem iso_hom : homomorphism natural_isomorphism.
+Theorem hom_nat_iso : homomorphism natural_isomorphism.
 Proof.
 unfold homomorphism, natural_isomorphism; split;
 [exact natural_isomorphism_0 | exact natural_isomorphism_succ].
@@ -51,61 +51,59 @@ Qed.
 
 End Homomorphism.
 
-Module Inverse (Nat1 Nat2 : NBaseSig).
+Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
 
-Module Import NBasePropMod1 := NBasePropFunct Nat1.
+Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1.
 (* This makes the tactic induct available. Since it is taken from
-NBasePropFunct Nat1, it refers to Nat1.induction. *)
+(NBasePropFunct NAxiomsMod1), it refers to induction on N1. *)
 
-Module Hom12 := Homomorphism Nat1 Nat2.
-Module Hom21 := Homomorphism Nat2 Nat1.
+Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
+Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.
 
-Notation Local N1 := Nat1.NDomainModule.N.
-Notation Local N2 := Nat2.NDomainModule.N.
+Notation Local N1 := NAxiomsMod1.N.
+Notation Local N2 := NAxiomsMod2.N.
 Notation Local h12 := Hom12.natural_isomorphism.
 Notation Local h21 := Hom21.natural_isomorphism.
 
-Notation Local "x == y" := (Nat1.NDomainModule.E x y) (at level 70).
+Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity).
 
-Lemma iso_inverse :
-  forall x : N1, h21 (h12 x) == x.
+Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n.
 Proof.
-induct x.
-now rewrite Hom12.natural_isomorphism_0; rewrite Hom21.natural_isomorphism_0.
-intros x IH.
-rewrite Hom12.natural_isomorphism_succ; rewrite Hom21.natural_isomorphism_succ;
-now rewrite IH.
+induct n.
+now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0.
+intros n IH.
+now rewrite Hom12.natural_isomorphism_succ, Hom21.natural_isomorphism_succ, IH.
 Qed.
 
 End Inverse.
 
-Module Isomorphism (Nat1 Nat2 : NBaseSig).
+Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
 
-Module Hom12 := Homomorphism Nat1 Nat2.
-Module Hom21 := Homomorphism Nat2 Nat1.
+Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
+Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.
 
-Module Inverse121 := Inverse Nat1 Nat2.
-Module Inverse212 := Inverse Nat2 Nat1.
+Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2.
+Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1.
 
-Notation Local N1 := Nat1.NDomainModule.N.
-Notation Local N2 := Nat2.NDomainModule.N.
-Notation Local E1 := Nat1.NDomainModule.E.
-Notation Local E2 := Nat2.NDomainModule.E.
+Notation Local N1 := NAxiomsMod1.N.
+Notation Local N2 := NAxiomsMod2.N.
+Notation Local Eq1 := NAxiomsMod1.Neq.
+Notation Local Eq2 := NAxiomsMod2.Neq.
 Notation Local h12 := Hom12.natural_isomorphism.
 Notation Local h21 := Hom21.natural_isomorphism.
 
 Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop :=
   Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\
-  forall x : N1, E1 (f2 (f1 x)) x /\
-  forall y : N2, E2 (f1 (f2 y)) y.
+  forall n : N1, Eq1 (f2 (f1 n)) n /\
+  forall n : N2, Eq2 (f1 (f2 n)) n.
 
-Theorem iso_iso : isomorphism h12 h21.
+Theorem iso_nat_iso : isomorphism h12 h21.
 Proof.
 unfold isomorphism.
-split. apply Hom12.iso_hom.
-split. apply Hom21.iso_hom.
-split. apply Inverse121.iso_inverse.
-apply Inverse212.iso_inverse.
+split. apply Hom12.hom_nat_iso.
+split. apply Hom21.hom_nat_iso.
+split. apply Inverse12.inverse_nat_iso.
+apply Inverse21.inverse_nat_iso.
 Qed.
 
 End Isomorphism.
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 07fc67499..5ac1f70fb 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -2,7 +2,11 @@ Require Export NTimesOrder.
 
 Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope NatScope.
+
+Theorem minus_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2.
+Proof NZminus_wd.
 
 Theorem minus_0_r : forall n : N, n - 0 == n.
 Proof NZminus_0_r.
diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v
deleted file mode 100644
index 4333d9e46..000000000
--- a/theories/Numbers/Natural/Abstract/NMiscFunct.v
+++ /dev/null
@@ -1,398 +0,0 @@
-Require Import Bool. (* To get the orb and negb function *)
-Require Export NStrongRec.
-Require Export NTimesOrder.
-
-Module MiscFunctFunctor (Import NatMod : NBaseSig).
-Module Export StrongRecPropertiesModule := StrongRecProperties NatMod.
-Open Local Scope NatScope.
-
-(*****************************************************)
-(**                   Addition                       *)
-
-Definition plus (x y : N) := recursion y (fun _ p => S p) x.
-
-Lemma plus_step_wd : fun2_wd E E E (fun _ p => S p).
-Proof.
-unfold fun2_wd; intros _ _ _ p p' H; now rewrite H.
-Qed.
-
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
-Proof.
-unfold plus.
-intros x x' Exx' y y' Eyy'.
-apply recursion_wd with (EA := E).
-assumption.
-unfold eq_fun2; intros _ _ _ p p' Epp'; now rewrite Epp'.
-assumption.
-Qed.
-
-Theorem plus_0 : forall y, plus 0 y == y.
-Proof.
-intro y. unfold plus.
-(*pose proof (recursion_0 E y (fun _ p => S p)) as H.*)
-rewrite recursion_0. apply (proj1 E_equiv).
-Qed.
-
-Theorem plus_succ : forall x y, plus (S x) y == S (plus x y).
-Proof.
-intros x y; unfold plus.
-now rewrite (recursion_succ E); [|apply plus_step_wd|].
-Qed.
-
-(*****************************************************)
-(**                  Multiplication                  *)
-
-Definition times (x y : N) := recursion 0 (fun _ p => plus p x) y.
-
-Lemma times_step_wd : forall x, fun2_wd E E E (fun _ p => plus p x).
-Proof.
-unfold fun2_wd. intros. now apply plus_wd.
-Qed.
-
-Lemma times_step_equal :
-  forall x x', x == x' -> eq_fun2 E E E (fun _ p => plus p x) (fun x p => plus p x').
-Proof.
-unfold eq_fun2; intros; apply plus_wd; assumption.
-Qed.
-
-Add Morphism times with signature E ==> E ==> E as times_wd.
-Proof.
-unfold times.
-intros x x' Exx' y y' Eyy'.
-apply recursion_wd with (EA := E).
-reflexivity. apply times_step_equal. assumption. assumption.
-Qed.
-
-Theorem times_0_r : forall x, times x 0 == 0.
-Proof.
-intro. unfold times. now rewrite recursion_0.
-Qed.
-
-Theorem times_succ_r : forall x y, times x (S y) == plus (times x y) x.
-Proof.
-intros x y; unfold times.
-now rewrite (recursion_succ E); [| apply times_step_wd |].
-Qed.
-
-(*****************************************************)
-(**                   Less Than                      *)
-
-Definition lt (m : N) : N -> bool :=
-  recursion (if_zero false true)
-            (fun _ f => fun n => recursion false (fun n' _ => f n') n)
-            m.
-
-(* It would be more efficient to make a three-way comparison, i.e.,
-return Eq, Lt, or Gt, but since these are no-use default functions,
-we define <= as (< or =) *)
-Definition le (n m : N) := lt n m || e n m.
-
-Theorem le_lt : forall n m, le n m <-> lt n m \/ n == m.
-Proof.
-intros n m. rewrite E_equiv_e. unfold le.
-do 3 rewrite eq_true_unfold_pos.
-assert (H : lt n m || e n m = true <-> lt n m = true \/ e n m = true).
-split; [apply orb_prop | apply orb_true_intro].
-now rewrite H.
-Qed.
-
-Theorem le_intro_left : forall n m, lt n m -> le n m.
-Proof.
-intros; rewrite le_lt; now left.
-Qed.
-
-Theorem le_intro_right : forall n m, n == m -> le n m.
-Proof.
-intros; rewrite le_lt; now right.
-Qed.
-
-Lemma lt_base_wd : eq_fun E eq_bool (if_zero false true) (if_zero false true).
-unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_succet.
-Qed.
-
-Lemma lt_step_wd :
-  let step := (fun _ f => fun n => recursion false (fun n' _ => f n') n) in
-    eq_fun2 E (eq_fun E eq_bool) (eq_fun E eq_bool) step step.
-Proof.
-unfold eq_fun2, eq_fun, eq_bool.
-intros x x' Exx' f f' Eff' y y' Eyy'.
-apply recursion_wd with (EA := eq_bool); unfold eq_bool.
-reflexivity.
-unfold eq_fun2; intros; now apply Eff'.
-assumption.
-Qed.
-
-Lemma lt_curry_wd : forall m m', m == m' -> eq_fun E eq_bool (lt m) (lt m').
-Proof.
-unfold lt.
-intros m m' Emm'.
-apply recursion_wd with (EA := eq_fun E eq_bool).
-apply lt_base_wd.
-apply lt_step_wd.
-assumption.
-Qed.
-
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
-Proof.
-unfold eq_fun; intros m m' Emm' n n' Enn'.
-now apply lt_curry_wd.
-Qed.
-
-(* Note that if we unfold lt along with eq_fun above, then "apply" signals
-as error "Impossible to unify", not just, e.g., "Cannot solve second-order
-unification problem". Something is probably wrong. *)
-
-Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
-Proof.
-intros x1 x2 H1 x3 x4 H2; unfold le; rewrite H1; now rewrite H2.
-Qed.
-
-Theorem lt_base_eq : forall n, lt 0 n = if_zero false true n.
-Proof.
-intro n; unfold lt; now rewrite recursion_0.
-Qed.
-
-Theorem lt_step_eq : forall m n, lt (S m) n = recursion false (fun n' _ => lt m n') n.
-Proof.
-intros m n; unfold lt.
-pose proof (recursion_succ (eq_fun E eq_bool) (if_zero false true)
-  (fun _ f => fun n => recursion false (fun n' _ => f n') n)
-  lt_base_wd lt_step_wd m n n) as H.
-unfold eq_bool in H.
-assert (H1 : n == n); [reflexivity | apply H in H1; now rewrite H1].
-Qed.
-
-Theorem lt_0 : forall n, ~ lt n 0.
-Proof.
-ases/g
-rewrite lt_base_eq; rewrite if_zero_0; now intro.
-intros n; rewrite lt_step_eq. rewrite recursion_0. now intro.
-Qed.
-
-(* Above, we rewrite applications of function. Is it possible to rewrite
-functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
-lt_step n (recursion lt_base lt_step n)? *)
-
-Lemma lt_0_1 : lt 0 1.
-Proof.
-rewrite lt_base_eq; now rewrite if_zero_succ.
-Qed.
-
-Lemma lt_0_succn : forall n, lt 0 (S n).
-Proof.
-intro n; rewrite lt_base_eq; now rewrite if_zero_succ.
-Qed.
-
-Lemma lt_succn_succm : forall n m, lt (S n) (S m) <-> lt n m.
-Proof.
-intros n m.
-rewrite lt_step_eq. rewrite (recursion_succ eq_bool).
-reflexivity.
-now unfold eq_bool.
-unfold fun2_wd; intros; now apply lt_wd.
-Qed.
-
-Theorem lt_succ : forall m n, lt m (S n) <-> le m n.
-Proof.
-assert (A : forall m n, lt m (S n) <-> lt m n \/ m == n).
-induct m.
-ases/g
-[split; intro; [now right | apply lt_0_1] |
-intro n; split; intro; [left |]; apply lt_0_succn].
-ases/g
-split.
-intro. assert (H1 : lt n 0); [now apply -> lt_succn_succm | false_hyp H1 lt_0].
-intro H; destruct H as [H | H].
-false_hyp H lt_0. false_hyp H succ_0.
-intro m. pose proof (IH m) as H; clear IH.
-assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_succn_succm |].
-assert (lt (S n) (S m) <-> lt n m); [apply lt_succn_succm |].
-assert (S n == S m <-> n == m); [split; [ apply succ_inj | apply succ_wd]|]. tauto.
-intros; rewrite le_lt; apply A.
-Qed.
-
-(*****************************************************)
-(**                     Even                         *)
-
-Definition even (x : N) := recursion true (fun _ p => negb p) x.
-
-Lemma even_step_wd : fun2_wd E eq_bool eq_bool (fun x p => if p then false else true).
-Proof.
-unfold fun2_wd.
-intros x x' Exx' b b' Ebb'.
-unfold eq_bool; destruct b; destruct b'; now simpl.
-Qed.
-
-Add Morphism even with signature E ==> eq_bool as even_wd.
-Proof.
-unfold even; intros.
-apply recursion_wd with (A := bool) (EA := eq_bool).
-now unfold eq_bool.
-unfold eq_fun2. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl.
-assumption.
-Qed.
-
-Theorem even_0 : even 0 = true.
-Proof.
-unfold even.
-now rewrite recursion_0.
-Qed.
-
-Theorem even_succ : forall x : N, even (S x) = negb (even x).
-Proof.
-unfold even.
-intro x; rewrite (recursion_succ (@eq bool)); try reflexivity.
-unfold fun2_wd.
-intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl.
-Qed.
-
-(*****************************************************)
-(**                Division by 2                     *)
-
-Definition half_aux (x : N) : N * N :=
-  recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x.
-
-Definition half (x : N) := snd (half_aux x).
-
-Definition E2 := prod_rel E E.
-
-Add Relation (prod N N) E2
-reflexivity proved by (prod_rel_refl N N E E E_equiv E_equiv)
-symmetry proved by (prod_rel_symm N N E E E_equiv E_equiv)
-transitivity proved by (prod_rel_trans N N E E E_equiv E_equiv)
-as E2_rel.
-
-Lemma half_step_wd: fun2_wd E E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))).
-Proof.
-unfold fun2_wd, E2, prod_rel.
-intros _ _ _ p1 p2 [H1 H2].
-destruct p1; destruct p2; simpl in *.
-now split; [rewrite H2 |].
-Qed.
-
-Add Morphism half with signature E ==> E as half_wd.
-Proof.
-unfold half.
-assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)).
-intros x y Exy; unfold half_aux; apply recursion_wd with (EA := E2); unfold E2.
-unfold E2.
-unfold prod_rel; simpl; now split.
-unfold eq_fun2, prod_rel; simpl.
-intros _ _ _ p1 p2; destruct p1; destruct p2; simpl.
-intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption.
-unfold E2, prod_rel in H. intros x y Exy; apply H in Exy.
-exact (proj2 Exy).
-Qed.
-
-(*****************************************************)
-(**            Logarithm for the base 2              *)
-
-Definition log (x : N) : N :=
-strong_rec 0
-           (fun x g =>
-              if (e x 0) then 0
-              else if (e x 1) then 0
-              else S (g (half x)))
-           x.
-
-Add Morphism log with signature E ==> E as log_wd.
-Proof.
-intros x x' Exx'. unfold log.
-apply strong_rec_wd with (EA := E); try (reflexivity || assumption).
-unfold eq_fun2. intros y y' Eyy' g g' Egg'.
-assert (H : e y 0 = e y' 0); [now apply e_wd|].
-rewrite <- H; clear H.
-assert (H : e y 1 = e y' 1); [now apply e_wd|].
-rewrite <- H; clear H.
-assert (H : S (g (half y)) == S (g' (half y')));
-[apply succ_wd; apply Egg'; now apply half_wd|].
-now destruct (e y 0); destruct (e y 1).
-Qed.
-
-(*********************************************************)
-(** To get the properties of plus, times and lt defined  *)
-(** via recursion, we form the corresponding modules and *)
-(** apply the properties functors to these modules       *)
-
-Module NDefaultPlusModule <: NPlusSig.
-
-Module NBaseMod := NatMod.
-(* If we used the name NBaseMod instead of NatMod then this would
-produce many warnings like "Trying to mask the absolute name
-NBaseMod", "Trying to mask the absolute name Nat.O" etc. *)
-
-Definition plus := plus.
-
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
-Proof.
-exact plus_wd.
-Qed.
-
-Theorem plus_0_l : forall n, plus 0 n == n.
-Proof.
-exact plus_0.
-Qed.
-
-Theorem plus_succ_l : forall n m, plus (S n) m == S (plus n m).
-Proof.
-exact plus_succ.
-Qed.
-
-End NDefaultPlusModule.
-
-Module NDefaultTimesModule <: NTimesSig.
-Module NPlusMod := NDefaultPlusModule.
-
-Definition times := times.
-
-Add Morphism times with signature E ==> E ==> E as times_wd.
-Proof.
-exact times_wd.
-Qed.
-
-Definition times_0_r := times_0_r.
-Definition times_succ_r := times_succ_r.
-
-End NDefaultTimesModule.
-
-Module NDefaultOrderModule <: NOrderSig.
-Module NBaseMod := NatMod.
-
-Definition lt := lt.
-Definition le := le.
-
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
-Proof.
-exact lt_wd.
-Qed.
-
-Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
-Proof.
-exact le_wd.
-Qed.
-
-(* This produces a warning about a morphism redeclaration. Why is not
-there a warning after declaring lt? *)
-
-Theorem le_lt : forall x y, le x y <-> lt x y \/ x == y.
-Proof.
-exact le_lt.
-Qed.
-
-Theorem lt_0 : forall x, ~ (lt x 0).
-Proof.
-exact lt_0.
-Qed.
-
-Theorem lt_succ : forall x y, lt x (S y) <-> le x y.
-Proof.
-exact lt_succ.
-Qed.
-
-End NDefaultOrderModule.
-
-Module Export DefaultTimesOrderProperties :=
-  NTimesOrderProperties NDefaultTimesModule NDefaultOrderModule.
-
-End MiscFunctFunctor.
-
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 7c2610ccc..3e338825e 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -2,12 +2,20 @@ Require Export NTimes.
 
 Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope NatScope.
 
 (* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *)
 
 (* Axioms *)
 
+Theorem lt_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 < m1 <-> n2 < m2).
+Proof NZlt_wd.
+
+Theorem le_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
+Proof NZle_wd.
+
 Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n == m.
 Proof NZle_lt_or_eq.
 
@@ -142,21 +150,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem right_induction :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
         forall n : N, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem left_induction :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N, A z ->
       (forall n : N, n < z -> A (S n) -> A n) ->
         forall n : N, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem order_induction :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
       (forall n : N, n < z  -> A (S n) -> A n) ->
@@ -164,7 +172,7 @@ Theorem order_induction :
 Proof NZorder_induction.
 
 Theorem right_induction' :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N,
       (forall n : N, n <= z -> A n) ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
@@ -172,7 +180,7 @@ Theorem right_induction' :
 Proof NZright_induction'.
 
 Theorem strong_right_induction' :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N,
       (forall n : N, n <= z -> A n) ->
       (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
@@ -182,7 +190,7 @@ Proof NZstrong_right_induction'.
 (** Elimintation principle for < *)
 
 Theorem lt_ind :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     forall n : N,
       A (S n) ->
       (forall m : N, n < m -> A m -> A (S m)) ->
@@ -192,7 +200,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem le_ind :
-  forall A : N -> Prop, predicate_wd E A ->
+  forall A : N -> Prop, predicate_wd Neq A ->
     forall n : N,
       A n ->
       (forall m : N, n <= m -> A m -> A (S m)) ->
@@ -258,9 +266,9 @@ Section RelElim.
 (* FIXME: Variable R : relation N. -- does not work *)
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd E E R.
+Hypothesis R_wd : rel_wd Neq Neq R.
 
-Add Morphism R with signature E ==> E ==> iff as R_morph2.
+Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
 Proof R_wd.
 
 Theorem le_ind_rel :
diff --git a/theories/Numbers/Natural/Abstract/NOtherInd.v b/theories/Numbers/Natural/Abstract/NOtherInd.v
deleted file mode 100644
index 7faae620a..000000000
--- a/theories/Numbers/Natural/Abstract/NOtherInd.v
+++ /dev/null
@@ -1,161 +0,0 @@
-Require Export NDomain.
-Declare Module Export NDomainModule : NDomainSignature.
-Open Local Scope NatScope.
-
-Parameter O : N.
-Parameter S : N -> N.
-
-Notation "0" := O.
-
-Definition induction :=
-forall P : N -> Prop, predicate_wd E P ->
-    P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n.
-
-Definition other_induction :=
-forall P : N -> Prop,
-  (forall n : N, n == 0 -> P n) ->
-  (forall n : N, P n -> forall m : N, m == S n -> P m) ->
-  forall n : N, P n.
-
-Theorem other_ind_implies_ind : other_induction -> induction.
-Proof.
-unfold induction, other_induction; intros OI P predicate_wd Base Step.
-apply OI; unfold predicate_wd in predicate_wd.
-intros; now apply -> (predicate_wd 0).
-intros n Pn m EmSn; now apply -> (predicate_wd (S n)); [apply Step|].
-Qed.
-
-Theorem ind_implies_other_ind : induction -> other_induction.
-Proof.
-intros I P Base Step.
-set (A := fun n => forall m, m == n -> P m).
-cut (forall n, A n).
-unfold A; intros H n; now apply (H n).
-apply I.
-unfold predicate_wd, A. intros x y Exy.
-split; intros H m Em; apply H; [now rewrite Exy | now rewrite <- Exy].
-exact Base.
-intros n Qn m EmSn; now apply Step with (n := n); [apply Qn |].
-Qed.
-
-(* This theorem is not really needed. It shows that if we have
-other_induction and we proved the base case and the induction step, we
-can in fact show that the predicate in question is well-defined, and
-therefore we can turn this other induction into the standard one. *)
-Theorem other_ind_implies_predicate_wd :
-other_induction ->
-  forall P : N -> Prop,
-    (forall n : N, n == 0 -> P n) ->
-    (forall n : N, P n -> forall m : N, m == S n -> P m) ->
-    predicate_wd E P.
-Proof.
-intros OI P Base Step; unfold predicate_wd.
-intros x; pattern x; apply OI; clear x.
-(* Base case *)
-intros x H1 y H2.
-assert (y == 0); [rewrite <- H2; now rewrite H1|].
-assert (P x); [now apply Base|].
-assert (P y); [now apply Base|].
-split; now intro.
-(* Step *)
-intros x IH z H y H1.
-rewrite H in H1. symmetry in H1.
-split; (intro H2; eapply Step; [|apply H || apply H1]); now apply OI.
-Qed.
-
-Section Recursion.
-
-Variable A : Set.
-Variable EA : relation A.
-Hypothesis EA_symm : symmetric A EA.
-Hypothesis EA_trans : transitive A EA.
-
-Add Relation A EA
- symmetry proved by EA_symm
- transitivity proved by EA_trans
-as EA_rel.
-
-Lemma EA_neighbor : forall a a' : A, EA a a' -> EA a a.
-Proof.
-intros a a' EAaa'.
-apply EA_trans with (y := a'); [assumption | apply EA_symm; assumption].
-Qed.
-
-Parameter recursion : A -> (N -> A -> A) -> N -> A.
-
-Axiom recursion_0 :
-  forall (a : A) (f : N -> A -> A),
-    EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a.
-
-Axiom recursion_succ :
-  forall (a : A) (f : N -> A -> A),
-    EA a a -> fun2_wd E EA EA f ->
-      forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
-
-Theorem recursion_wd : induction ->
-  forall a a' : A, EA a a' ->
-    forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
-      forall x x' : N, x == x' ->
-        EA (recursion a f x) (recursion a' f' x').
-Proof.
-intros I a a' Eaa' f f' f_wd f'_wd Eff'.
-apply ind_implies_other_ind in I.
-intro x; pattern x; apply I; clear x.
-intros x Ex0 x' Exx'.
-rewrite Ex0 in Exx'; symmetry in Exx'.
-(* apply recursion_0 in Ex0. produces
-Anomaly: type_of: this is not a well-typed term. Please report. *)
-assert (EA (recursion a f x) a).
-apply recursion_0. now apply EA_neighbor with (a' := a'). assumption.
-assert (EA a' (recursion a' f' x')).
-apply EA_symm. apply recursion_0. now apply EA_neighbor with (a' := a). assumption.
-apply EA_trans with (y := a). assumption.
-now apply EA_trans with (y := a').
-intros x IH y H y' H1.
-rewrite H in H1; symmetry in H1.
-assert (EA (recursion a f y) (f x (recursion a f x))).
-apply recursion_succ. now apply EA_neighbor with (a' := a').
-assumption. now symmetry.
-assert (EA (f' x (recursion a' f' x)) (recursion a' f' y')).
-symmetry; apply recursion_succ. now apply EA_neighbor with (a' := a). assumption.
-now symmetry.
-assert (EA (f x (recursion a f x)) (f' x (recursion a' f' x))).
-apply Eff'. reflexivity. apply IH. reflexivity.
-apply EA_trans with (y := (f x (recursion a f x))). assumption.
-apply EA_trans with (y := (f' x (recursion a' f' x))). assumption.
-assumption.
-Qed.
-
-Axiom recursion_0' :
-  forall (a : A) (f : N -> A -> A),
-    forall x : N, x == 0 -> recursion a f x = a.
-
-Axiom recursion_succ' :
-  forall (a : A) (f : N -> A -> A),
-    EA a a -> fun2_wd E EA EA f ->
-      forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)).
-
-Theorem recursion_wd' : other_induction ->
-  forall a a' : A, EA a a -> EA a' a' -> EA a a' ->
-    forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' ->
-      forall x x' : N, x == x' ->
-        EA (recursion a f x) (recursion a' f' x').
-Proof.
-intros I a a' a_wd a'_wd Eaa' f f' f_wd f'_wd Eff'.
-intro x; pattern x; apply I; clear x.
-intros x Ex0 x' Exx'. rewrite Ex0 in Exx'. symmetry in Exx'.
-replace (recursion a f x) with a. replace (recursion a' f' x') with a'.
-assumption. symmetry; now apply recursion_0'. symmetry; now apply recursion_0'.
-intros x IH y EySx y' Eyy'. rewrite EySx in Eyy'. symmetry in Eyy'.
-apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_succ'.
-apply EA_trans with (y := (f' x (recursion a' f' x))).
-apply Eff'. reflexivity. now apply IH.
-symmetry; now apply recursion_succ'.
-Qed.
-
-
-
-End Recursion.
-
-Implicit Arguments recursion [A].
-
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 8ca3ba000..1e5c2211f 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -2,7 +2,11 @@ Require Export NBase.
 
 Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope NatScope.
+
+Theorem plus_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2.
+Proof NZplus_wd.
 
 Theorem plus_0_l : forall n : N, 0 + n == n.
 Proof NZplus_0_l.
diff --git a/theories/Numbers/Natural/Abstract/NPred.v b/theories/Numbers/Natural/Abstract/NPred.v
deleted file mode 100644
index d3d22651c..000000000
--- a/theories/Numbers/Natural/Abstract/NPred.v
+++ /dev/null
@@ -1,46 +0,0 @@
-Require Export NAxioms.
-
-(* We would like to have a signature for the predecessor: first, to be
-able to provide an efficient implementation, and second, to be able to
-use this function in the signatures defining other functions, e.g.,
-subtraction. If we just define predecessor by recursion in
-NBasePropFunct functor, we would not be able to use it in other
-signatures. *)
-
-Module Type NPredSignature.
-Declare Module Export NBaseMod : NBaseSig.
-Open Local Scope NatScope.
-
-Parameter Inline P : N -> N.
-
-Add Morphism P with signature E ==> E as pred_wd.
-
-Axiom pred_0 : P 0 == 0.
-Axiom pred_succ : forall n, P (S n) == n.
-
-End NPredSignature.
-
-Module NDefPred (Import NM : NBaseSig) <: NPredSignature.
-Module NBaseMod := NM.
-Open Local Scope NatScope.
-
-Definition P (n : N) : N := recursion 0 (fun m _ : N => m) n.
-
-Add Morphism P with signature E ==> E as pred_wd.
-Proof.
-intros; unfold P.
-now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |].
-Qed.
-
-Theorem pred_0 : P 0 == 0.
-Proof.
-unfold P; now rewrite recursion_0.
-Qed.
-
-Theorem pred_succ : forall n, P (S n) == n.
-Proof.
-intro n; unfold P; now rewrite (recursion_succ E); [| unfold fun2_wd; now intros |].
-Qed.
-
-End NDefPred.
-
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
deleted file mode 100644
index d1f4aac26..000000000
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ /dev/null
@@ -1,69 +0,0 @@
-Require Export NAxioms.
-
-Module StrongRecProperties (Import NBaseMod : NBaseSig).
-Module Export NBasePropMod := NBasePropFunct NBaseMod.
-Open Local Scope NatScope.
-
-Section StrongRecursion.
-
-Variable A : Set.
-Variable EA : relation A.
-
-Hypothesis EA_equiv : equiv A EA.
-
-Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (x : N) : A :=
-(recursion (fun _ : N => a)
-           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
-           (S x)) x.
-
-Lemma strong_rec_step_wd : forall f : N -> (N -> A) -> A,
-fun2_wd E (eq_fun E EA) EA f ->
-  fun2_wd E (eq_fun E EA) (eq_fun E EA)
-    (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)).
-Proof.
-unfold fun2_wd; intros f f_wd.
-intros x x' Exx'. unfold eq_fun. intros g g' Egg' y y' Eyy'.
-assert (H : e y x = e y' x'). now apply e_wd. rewrite H.
-destruct (e y' x'); simpl.
-now apply f_wd. now apply Egg'.
-Qed.
-
-Theorem strong_rec_wd :
-forall a a', EA a a' ->
-  forall f f', eq_fun2 E (eq_fun E EA) EA f f' ->
-    forall x x', x == x' ->
-      EA (strong_rec a f x) (strong_rec a' f' x').
-Proof.
-intros a a' Eaa' f f' Eff' x x' Exx'.
-assert (H : eq_fun E EA
-  (recursion (fun _ : N => a)
-           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y))
-           (S x))
-  (recursion (fun _ : N => a')
-           (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f' x p) else (p y))
-           (S x'))).
-apply recursion_wd with (EA := eq_fun E EA).
-unfold eq_fun; now intros.
-unfold eq_fun2. intros y y' Eyy' p p' Epp'. unfold eq_fun. intros z z' Ezz'.
-assert (H: e z y = e z' y'); [now apply e_wd|].
-rewrite <- H. destruct (e z y); [now apply Eff' | now apply Epp'].
-now rewrite Exx'.
-unfold strong_rec.
-now apply H.
-Qed.
-
-(* To do:
-Definition step_good (g : N -> (N -> A) -> A) :=
-  forall (x : N) (h1 h2 : N -> A),
-    (forall y : N, y < x -> EA (h1 y) (h2 y)) -> EA (g x h1) (g x h2).
-
-Theorem strong_recursion_fixpoint : forall a g, step_good g ->
-  let f x := (strong_rec a g x) in forall x, EA (f x) (g x f).
-*)
-
-End StrongRecursion.
-
-Implicit Arguments strong_rec [A].
-
-End StrongRecProperties.
-
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index bcf073ffa..76b85ee87 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -5,7 +5,11 @@ Require Export NPlus.
 
 Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope NatScope.
+
+Theorem times_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2.
+Proof NZtimes_wd.
 
 Theorem times_0_r : forall n, n * 0 == 0.
 Proof NZtimes_0_r.
@@ -39,7 +43,7 @@ Proof NZtimes_1_l.
 Theorem times_1_r : forall n : N, n * 1 == n.
 Proof NZtimes_1_r.
 
-Lemma Nsemi_ring : semi_ring_theory 0 1 NZplus NZtimes E.
+Lemma Nsemi_ring : semi_ring_theory 0 1 NZplus NZtimes Neq.
 Proof.
 constructor.
 exact plus_0_l.
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index dc1b977aa..e644304dc 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -2,7 +2,7 @@ Require Export NOrder.
 
 Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope NatScope.
 
 Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
 Proof NZplus_lt_mono_l.