An update on theories/Numbers.

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

10 files changed, 298 insertions, 575 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
new file mode 100644
index 0000000000..a30c816822
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -0,0 +1,39 @@
+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).
+
+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' ->
+      forall x x' : N, x == x' ->
+        EA (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)).
+
+End NAxiomsSig.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index b8940027c0..b999240fb8 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -2,13 +2,12 @@ Require Export NAxioms.
 Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *)
 
 Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig).
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 (* 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
 only one time. *)
 
-Module NZOrdAxiomsMod := NNZFunct NAxiomsMod.
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
 (* Here we probably need to re-prove all axioms declared in NAxioms.v to
@@ -20,20 +19,12 @@ 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). *)
 
-Theorem E_equiv : equiv N E.
-Proof E_equiv.
-
-Theorem induction :
-  forall A : N -> Prop, predicate_wd E A ->
-    A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
-Proof induction.
+Theorem pred_succ : forall n : N, P (S n) == n.
+Proof NZpred_succ.
 
 Theorem pred_0 : P 0 == 0.
 Proof pred_0.
 
-Theorem pred_succ : forall n : N, P (S n) == n.
-Proof pred_succ.
-
 Theorem neq_symm : forall n m : N, n ~= m -> m ~= n.
 Proof NZneq_symm.
 
@@ -46,37 +37,79 @@ Proof NZsucc_inj_wd.
 Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
+(* Now we prove that the successor of a number is not zero by defining a
+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.
+Proof.
+intros; unfold if_zero. apply recursion_wd with (EA := (@eq A)).
+reflexivity. unfold eq_fun2; now intros. assumption.
+Qed.
+
+Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
+Proof.
+unfold if_zero; intros; now rewrite recursion_0.
+Qed.
+
+Theorem if_zero_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b.
+Proof.
+intros; unfold if_zero.
+now rewrite (@recursion_succ A (@eq A)); [| | unfold fun2_wd; now intros].
+Qed.
+
+Implicit Arguments if_zero [A].
+
+Theorem neq_succ_0 : forall n : N, ~ S n == 0.
+Proof.
+intros n H.
+assert (true = false); [| discriminate].
+replace true with (if_zero false true (S n)) by apply if_zero_succ.
+pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0.
+now rewrite H.
+Qed.
+
+(* Next, we show that all numbers are nonnegative and recover regular induction
+from the bidirectional induction on NZ *)
+
+Theorem le_0_l : forall n : N, 0 <= n.
+Proof.
+NZinduct n.
+le_equal.
+intro n; split.
+apply NZle_le_succ.
+intro H; apply -> NZle_succ_le_or_eq_succ in H; destruct H as [H | H].
+assumption.
+symmetry in H; false_hyp H neq_succ_0.
+Qed.
+
+Theorem induction :
+  forall A : N -> Prop, predicate_wd E 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.
+intros; auto; apply le_0_l. apply le_0_l.
+Qed.
+
 (* The theorems NZinduction, NZcentral_induction and the tactic NZinduct
-refer to bidirectional induction, which is not so useful on natural
+refer to bidirectional induction, which is not useful on natural
 numbers. Therefore, we define a new induction tactic for natural numbers.
 We do not have to call "Declare Left Step" and "Declare Right Step"
 commands again, since the data for stepl and stepr tactics is inherited
-from NZ. *)
+from N. *)
 
-Tactic Notation "induct" ident(n) := induction_maker n ltac:(apply induction).
-(* FIXME: "Ltac induct n := induction_maker n ltac:(apply induction)" does not work (bug 1703) *)
+Ltac induct n := induction_maker n ltac:(apply induction).
 
-(* Now we add properties peculiar to natural numbers *)
-
-Theorem nondep_induction :
+Theorem case_analysis :
   forall A : N -> Prop, predicate_wd E A ->
     A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
 Proof.
 intros; apply induction; auto.
 Qed.
 
-Tactic Notation "nondep_induct" ident(n) :=
-  induction_maker n ltac:(apply nondep_induction).
-
-(* The fact "forall n : N, S n ~= 0" can be proved either by building a
-function (using recursion) that maps 0 ans S n to two provably different
-terms, or from the axioms of order *)
-
-Theorem neq_succ_0 : forall n : N, S n ~= 0.
-Proof.
-intros n H. apply nlt_0_r with n. rewrite <- H.
-apply <- lt_succ_le. apply <- le_lt_or_eq. now right.
-Qed.
+Ltac cases n := induction_maker n ltac:(apply case_analysis).
 
 Theorem neq_0 : ~ forall n, n == 0.
 Proof.
@@ -85,19 +118,21 @@ Qed.
 
 Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m.
 Proof.
-nondep_induct n. split; intro H;
+cases n. split; intro H;
 [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0].
 intro n; split; intro H; [now exists n | apply neq_succ_0].
 Qed.
 
 Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m.
 Proof.
-nondep_induct n; [now left | intros n; right; now exists n].
+cases n.
+now left.
+intro n; right; now exists n.
 Qed.
 
 Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1.
 Proof.
-nondep_induct n.
+cases n.
 rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto.
 split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H].
 intro n. rewrite pred_succ. rewrite_false (S n == 0) neq_succ_0.
@@ -106,18 +141,18 @@ Qed.
 
 Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n.
 Proof.
-nondep_induct n.
+cases n.
 intro H; elimtype False; now apply H.
 intros; now rewrite pred_succ.
 Qed.
 
 Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 intros H; elimtype False; now apply H.
-intros n H1; nondep_induct m.
+intros n _; cases m.
 intros H; elimtype False; now apply H.
-intros m H2 H3. do 2 rewrite pred_succ in H3. now apply succ_wd.
+intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3.
 Qed.
 
 (* The following induction principle is useful for reasoning about, e.g.,
@@ -144,7 +179,7 @@ Qed.
 
 End PairInduction.
 
-Tactic Notation "pair_induct" ident(n) := induction_maker n ltac:(apply pair_induction).
+(*Ltac pair_induct n := induction_maker n ltac:(apply pair_induction).*)
 
 (* The following is useful for reasoning about, e.g., Ackermann function *)
 Section TwoDimensionalInduction.
@@ -171,11 +206,11 @@ Qed.
 
 End TwoDimensionalInduction.
 
-Tactic Notation "two_dim_induct" ident(n) ident(m) :=
+(*Ltac two_dim_induct n m :=
   try intros until n;
   try intros until m;
   pattern n, m; apply two_dim_induction; clear n m;
-  [solve_rel_wd | | | ].
+  [solve_rel_wd | | | ].*)
 
 Section DoubleInduction.
 
@@ -193,12 +228,12 @@ Theorem double_induction :
    (forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m.
 Proof.
 intros H1 H2 H3; induct n; auto.
-intros n IH; nondep_induct m; auto.
+intros n H; cases m; auto.
 Qed.
 
 End DoubleInduction.
 
-Tactic Notation "double_induct" ident(n) ident(m) :=
+Ltac double_induct n m :=
   try intros until n;
   try intros until m;
   pattern n, m; apply double_induction; clear n m;
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 0af5c22fd2..8111261239 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -2,13 +2,13 @@ Require Export NTimesOrder.
 
 Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 Theorem minus_0_r : forall n : N, n - 0 == n.
-Proof minus_0_r.
+Proof NZminus_0_r.
 
 Theorem minus_succ_r : forall n m : N, n - (S m) == P (n - m).
-Proof minus_succ_r.
+Proof NZminus_succ_r.
 
 Theorem minus_1_r : forall n : N, n - 1 == P n.
 Proof.
@@ -85,7 +85,7 @@ intros n m p H; double_induct n m.
 intros m H1; rewrite minus_0_l in H1. symmetry in H1; false_hyp H1 H.
 intro n; rewrite minus_0_r; now rewrite plus_0_l.
 intros n m IH H1. rewrite minus_succ in H1. apply IH in H1.
-rewrite plus_succ_l; now apply succ_wd.
+rewrite plus_succ_l; now rewrite H1.
 Qed.
 
 Theorem minus_plus_distr : forall n m p : N, n - (m + p) == (n - m) - p.
@@ -126,7 +126,7 @@ Qed.
 
 Theorem times_pred_r : forall n m : N, n * (P m) == n * m - n.
 Proof.
-intro n; nondep_induct m.
+intros n m; cases m.
 now rewrite pred_0, times_0_r, minus_0_l.
 intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
 le_equal.
diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v
index 82a9224533..362dc05164 100644
--- a/theories/Numbers/Natural/Abstract/NMiscFunct.v
+++ b/theories/Numbers/Natural/Abstract/NMiscFunct.v
@@ -164,7 +164,7 @@ Qed.
 
 Theorem lt_0 : forall n, ~ lt n 0.
 Proof.
-nondep_induct n.
+ases/g
 rewrite lt_base_eq; rewrite if_zero_0; now intro.
 intros n; rewrite lt_step_eq. rewrite recursion_0. now intro.
 Qed.
@@ -196,10 +196,10 @@ 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.
-nondep_induct n;
+ases/g
 [split; intro; [now right | apply lt_0_1] |
 intro n; split; intro; [left |]; apply lt_0_succn].
-intros n IH. nondep_induct n0.
+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].
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 773f5d97ee..e8311c63c4 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -2,20 +2,17 @@ Require Export NTimes.
 
 Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 (* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *)
 
 (* Axioms *)
 
 Theorem le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y.
-Proof le_lt_or_eq.
-
-Theorem nlt_0_r : forall x, ~ (x < 0).
-Proof nlt_0_r.
+Proof NZle_lt_or_eq.
 
 Theorem lt_succ_le : forall x y, x < S y <-> x <= y.
-Proof lt_succ_le.
+Proof NZlt_succ_le.
 
 (* Renaming theorems from NZOrder.v *)
 
@@ -195,11 +192,11 @@ Proof NZle_ind.
 
 (** Theorems that are true for natural numbers but not for integers *)
 
-Theorem le_0_l : forall n : N, 0 <= n.
+(* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
+
+Theorem nlt_0_r : forall n : N, ~ n < 0.
 Proof.
-induct n.
-now le_equal.
-intros; now apply le_le_succ.
+intro n; apply -> le_nlt. apply le_0_l.
 Qed.
 
 Theorem nle_succ_0 : forall n, ~ (S n <= 0).
@@ -228,19 +225,19 @@ Qed.
 
 Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
 Proof.
-nondep_induct n.
+cases n.
 split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
 intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
 Qed.
 
 Lemma Acc_nonneg_lt : forall n : N,
-  Acc (fun n m => 0 <= n /\ n < m) n -> Acc lt n.
+  Acc (fun n m => 0 <= n /\ n < m) n -> Acc NZlt n.
 Proof.
 intros n H; induction H as [n _ H2];
 constructor; intros y H; apply H2; split; [apply le_0_l | assumption].
 Qed.
 
-Theorem lt_wf : well_founded lt.
+Theorem lt_wf : well_founded NZlt.
 Proof.
 unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf.
 Qed.
@@ -296,14 +293,14 @@ Qed.
 
 Theorem le_pred_l : forall n : N, P n <= n.
 Proof.
-nondep_induct n.
+cases n.
 rewrite pred_0; le_equal.
 intros; rewrite pred_succ;  apply le_succ_r.
 Qed.
 
 Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.
 Proof.
-nondep_induct n.
+cases n.
 intro H; elimtype False; now apply H.
 intros; rewrite pred_succ;  apply lt_succ_r.
 Qed.
@@ -320,14 +317,14 @@ Qed.
 
 Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *)
 Proof.
-intro n; nondep_induct m.
+intro n; cases m.
 intro H; false_hyp H nlt_0_r.
 intros m IH. rewrite pred_succ; now apply -> lt_succ_le.
 Qed.
 
 Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *)
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 rewrite pred_0; intro H; le_less.
 intros n IH. rewrite pred_succ in IH. now apply -> lt_le_succ.
 Qed.
@@ -378,7 +375,7 @@ Qed.
 
 Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m.
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 rewrite pred_0. split; intro H; apply le_0_l.
 intro n. rewrite pred_succ. apply succ_le_mono.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 67a2766ba4..f1e0e6ace9 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -2,13 +2,13 @@ Require Export NBase.
 
 Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 Theorem plus_0_l : forall n : N, 0 + n == n.
-Proof plus_0_l.
+Proof NZplus_0_l.
 
 Theorem plus_succ_l : forall n m : N, (S n) + m == S (n + m).
-Proof plus_succ_l.
+Proof NZplus_succ_l.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
@@ -42,7 +42,7 @@ Proof NZplus_cancel_l.
 Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
 Proof NZplus_cancel_r.
 
-(** Theorems that are valid for natural numbers but cannot be proved for NZ *)
+(** Theorems that are valid for natural numbers but cannot be proved for N *)
 
 Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
@@ -58,7 +58,7 @@ Theorem plus_eq_succ :
   forall n m : N, (exists p : N, n + m == S p) <->
                     (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 split; intro H.
 destruct H as [p H]. rewrite plus_0_l in H; right; now exists p.
 destruct H as [[n' H] | [m' H]].
@@ -91,7 +91,7 @@ Qed.
 
 Theorem plus_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 intro H; now elim H.
 intros n IH; rewrite plus_succ_l; now do 2 rewrite pred_succ.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index 7d42a812ce..a0d255892b 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -5,13 +5,13 @@ Require Export NPlus.
 
 Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 Theorem times_0_r : forall n, n * 0 == 0.
-Proof times_0_r.
+Proof NZtimes_0_r.
 
 Theorem times_succ_r : forall n m, n * (S m) == n * m + n.
-Proof times_succ_r.
+Proof NZtimes_succ_r.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
@@ -39,7 +39,7 @@ Proof NZtimes_1_l.
 Theorem times_1_r : forall n : N, n * 1 == n.
 Proof NZtimes_1_r.
 
-Lemma semi_ring : semi_ring_theory 0 1 plus times E.
+Lemma semi_ring : semi_ring_theory 0 1 NZplus NZtimes E.
 Proof.
 constructor.
 exact plus_0_l.
@@ -97,9 +97,10 @@ Theorem plus_times_repl_pair : forall a n m n' m' u v,
   a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
 Proof.
 intros a n m n' m' u v H1 H2.
-apply (@times_wd a a) in H2; [| reflexivity].
-do 2 rewrite times_plus_distr_l in H2.
-symmetry in H2; add_equations H1 H2 as H3.
+apply (@NZtimes_wd a a) in H2; [| reflexivity].
+do 2 rewrite times_plus_distr_l in H2. symmetry in H2.
+assert (H3 : (a * n + u) + (a * n' + a * m) == (a * m + v) + (a * n + a * m'))
+  by now apply NZplus_wd.
 stepl (a * n + (u + a * n' + a * m)) in H3 by ring.
 stepr (a * n + (a * m + v + a * m')) in H3 by ring.
 apply -> plus_cancel_l in H3.
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 19b9e0ae42..68c6c4494f 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 NatScope.
+Open Local Scope NatIntScope.
 
 Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
 Proof NZplus_lt_mono_l.
@@ -48,7 +48,7 @@ Qed.
 
 Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m.
 Proof.
-intro n; nondep_induct m.
+intros n m; cases m.
 intro H; elimtype False; now apply H.
 intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r.
 Qed.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 165c1211f4..90b3387738 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -2,128 +2,106 @@ Require Import NArith.
 Require Import NMinus.
 
 Module NBinaryAxiomsMod <: NAxiomsSig.
-
 Open Local Scope N_scope.
-
-Definition N := N.
-Definition E := (@eq N).
-Definition O := 0.
-Definition S := Nsucc.
-
-(*Definition Npred (n : N) := match n with
-| 0 => 0
-| Npos p => match p with
-  | xH => 0
-  | _ => Npos (Ppred p)
-  end
-end.*)
-
-Definition P := Npred.
-Definition plus := Nplus.
-Definition minus := Nminus.
-
-(*Definition minus (n m : N) :=
-match n, m with
-| N0, _ => N0
-| n, N0 => n
-| Npos n', Npos m' =>
-  match Pminus_mask n' m' with
-  | IsPos p => Npos p
-  | _ => N0
-  end
-end.*)
-
-Definition times := Nmult.
-Definition lt := Nlt.
-Definition le := Nle.
-
-Theorem E_equiv : equiv N E.
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ := N.
+Definition NZE := (@eq N).
+Definition NZ0 := 0.
+Definition NZsucc := Nsucc.
+Definition NZpred := Npred.
+Definition NZplus := Nplus.
+Definition NZminus := Nminus.
+Definition NZtimes := Nmult.
+
+Theorem NZE_equiv : equiv N NZE.
 Proof (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.
+Add Relation N NZE
+ reflexivity proved by (proj1 NZE_equiv)
+ symmetry proved by (proj2 (proj2 NZE_equiv))
+ transitivity proved by (proj1 (proj2 NZE_equiv))
+as NZE_rel.
 
-Add Morphism S with signature E ==> E as succ_wd.
+Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism P with signature E ==> E as pred_wd.
+Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism times with signature E ==> E ==> E as times_wd.
+Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism lt with signature E ==> E ==> iff as lt_wd.
-Proof.
-unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism le with signature E ==> E ==> iff as le_wd.
-Proof.
-unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Theorem induction :
-  forall A : N -> Prop, predicate_wd E A ->
-    A 0 -> (forall n, A n -> A (Nsucc n)) -> forall n, A n.
+Theorem NZinduction :
+  forall A : N -> Prop, predicate_wd NZE A ->
+    A 0 -> (forall n, A n <-> A (Nsucc n)) -> forall n : N, A n.
 Proof.
-intros A predicate_wd; apply Nind.
+intros A A_wd A0 AS. apply Nind. assumption. intros; now apply -> AS.
 Qed.
 
-Theorem pred_0 : Npred 0 = 0.
-Proof.
-reflexivity.
-Qed.
-
-Theorem pred_succ : forall n : N, Npred (Nsucc n) = n.
+Theorem NZpred_succ : forall n : N, Npred (Nsucc n) = n.
 Proof.
 destruct n as [| p]; simpl. reflexivity.
 case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ).
 intro H; false_hyp H Psucc_not_one.
 Qed.
 
-Theorem plus_0_l : forall n : N, 0 + n = n.
+Theorem NZplus_0_l : forall n : N, 0 + n = n.
 Proof Nplus_0_l.
 
-Theorem plus_succ_l : forall n m : N, (Nsucc n) + m = Nsucc (n + m).
+Theorem NZplus_succ_l : forall n m : N, (Nsucc n) + m = Nsucc (n + m).
 Proof Nplus_succ.
 
-Theorem minus_0_r : forall n : N, n - 0 = n.
+Theorem NZminus_0_r : forall n : N, n - 0 = n.
 Proof Nminus_0_r.
 
-Theorem minus_succ_r : forall n m : N, n - (S m) = P (n - m).
+Theorem NZminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m).
 Proof Nminus_succ_r.
 
-Theorem times_0_r : forall n : N, n * 0 = 0.
+Theorem NZtimes_0_r : forall n : N, n * 0 = 0.
 Proof.
 intro n; rewrite Nmult_comm; apply Nmult_0_l.
 Qed.
 
-Theorem times_succ_r : forall n m : N, n * (Nsucc m) = n * m + n.
+Theorem NZtimes_succ_r : forall n m : N, n * (Nsucc m) = n * m + n.
 Proof.
 intros n m; rewrite Nmult_comm, Nmult_Sn_m.
 now rewrite Nplus_comm, Nmult_comm.
 Qed.
 
-Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m.
+End NZAxiomsMod.
+
+Definition NZlt := Nlt.
+Definition NZle := Nle.
+
+Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
+Proof.
+unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
+Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
+Proof.
+unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
+Qed.
+
+Theorem NZle_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m.
 Proof.
 intros n m.
 assert (H : (n ?= m) = Eq <-> n = m).
@@ -133,29 +111,37 @@ destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now
 now elim H1. destruct H1; discriminate.
 Qed.
 
-Theorem nlt_0_r : forall n : N, ~ (n < 0).
-Proof.
-unfold Nlt; destruct n as [| p]; simpl; discriminate.
-Qed.
+Theorem NZlt_irrefl : forall n : N, ~ n < n.
+Proof Nlt_irrefl.
 
-Theorem lt_succ_le : forall n m : N, n < (S m) <-> n <= m.
+Theorem NZlt_succ_le : forall n m : N, n < (Nsucc m) <-> n <= m.
 Proof.
-intros x y. rewrite le_lt_or_eq.
-unfold Nlt, Nle, S; apply Ncompare_n_Sm.
+intros x y. rewrite NZle_lt_or_eq.
+unfold Nlt, Nle; apply Ncompare_n_Sm.
 Qed.
 
+End NZOrdAxiomsMod.
+
 Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
   Nrec (fun _ => A) a f n.
 Implicit Arguments recursion [A].
 
+Theorem succ_neq_0 : forall n : N, Nsucc n <> 0.
+Proof Nsucc_0.
+
+Theorem pred_0 : Npred 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
 Theorem 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' ->
+    forall f f' : N -> A -> A, eq_fun2 NZE EA EA f f' ->
       forall x x' : N, x = x' ->
         EA (recursion a f x) (recursion a' f' x').
 Proof.
-unfold fun2_wd, E, eq_fun2.
+unfold fun2_wd, NZE, eq_fun2.
 intros A EA a a' Eaa' f f' Eff'.
 intro x; pattern x; apply Nind.
 intros x' H; now rewrite <- H.
@@ -173,10 +159,10 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
-    EA a a -> fun2_wd E EA EA f ->
+    EA a a -> fun2_wd NZE EA EA f ->
       forall n : N, EA (recursion a f (Nsucc n)) (f n (recursion a f n)).
 Proof.
-unfold E, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind.
+unfold NZE, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind.
 rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.
 clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
 now rewrite Nrect_step.
@@ -186,102 +172,8 @@ End NBinaryAxiomsMod.
 
 Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod.
 
-(*
-Module NBinaryDepRec <: NDepRecSignature.
-Module Export NDomainModule := NBinaryDomain.
-Module Export NBaseMod := BinaryNat.
-
-Definition dep_recursion := Nrec.
-
-Theorem 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.
-Proof.
-intros A a f; unfold dep_recursion; unfold Nrec; now rewrite Nrect_base.
-Qed.
-
-Theorem 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).
-Proof.
-intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step.
-Qed.
 
-End NBinaryDepRec.
-
-Module NBinaryPlus <: NPlusSig.
-Module Export NBaseMod := BinaryNat.
-
-Definition plus := Nplus.
-
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
-Proof.
-unfold E; congruence.
-Qed.
-
-End NBinaryPlus.
-
-Module NBinaryTimes <: NTimesSig.
-Module Export NPlusMod := NBinaryPlus.
-
-Definition times := Nmult.
-
-Add Morphism times with signature E ==> E ==> E as times_wd.
-Proof.
-unfold E; congruence.
-Qed.
-
-
-End NBinaryTimes.
-
-Module NBinaryOrder <: NOrderSig.
-Module Export NBaseMod := BinaryNat.
-
-Definition lt (m n : N) := comp_bool (Ncompare m n) Lt.
-Definition le (m n : N) := let c := (Ncompare m n) in orb (comp_bool c Lt) (comp_bool c Eq).
-
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
-Proof.
-unfold E; congruence.
-Qed.
-
-Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
-Proof.
-unfold E; congruence.
-Qed.
-
-Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m.
-Proof.
-intros n m.
-assert (H : (n ?= m) = Eq <-> n = m).
-(split; intro H); [now apply Ncompare_Eq_eq | rewrite H; apply Ncompare_refl].
-unfold le, lt; rewrite eq_true_or. repeat rewrite comp_bool_correct. now rewrite H.
-Qed.
-
-Theorem lt_0 : forall x, ~ (lt x 0).
-Proof.
-unfold lt; destruct x as [|x]; simpl; now intro.
-Qed.
-
-Theorem lt_succ : forall x y, lt x (S y) <-> le x y.
-Proof.
-intros x y. rewrite le_lt.
-assert (H1 : lt x (S y) <-> Ncompare x (S y) = Lt);
-[unfold lt, comp_bool; destruct (x ?= S y); simpl; split; now intro |].
-assert (H2 : lt x y <-> Ncompare x y = Lt);
-[unfold lt, comp_bool; destruct (x ?= y); simpl; split; now intro |].
-pose proof (Ncompare_n_Sm    m x y) as H. tauto.
-Qed.
-
-End NBinaryOrder.
-
-Module Export NBinaryTimesOrderProperties := NTimesOrderProperties NBinaryTimes NBinaryOrder.
-
-(* Todo: N implements NPred.v and NMinus.v *)
-
-(*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*)
-
-(* Just some fun comparing the efficiency of the generic log defined
+(* Some fun comparing the efficiency of the generic log defined
 by strong (course-of-value) recursion and the log defined by recursion
 on notation *)
 (* Time Eval compute in (log 100000). *) (* 98 sec *)
@@ -302,7 +194,7 @@ end.
 *)
 (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
 
-*)
+
 (*
  Local Variables:
  tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index aa5ac99cfe..2f6c13cac9 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -2,416 +2,175 @@ Require Import Arith.
 Require Import NMinus.
 
 Module NPeanoAxiomsMod <: NAxiomsSig.
-
-Definition N := nat.
-Definition E := (@eq nat).
-Definition O := 0.
-Definition S := S.
-Definition P := pred.
-Definition plus := plus.
-Definition minus := minus.
-Definition times := mult.
-Definition lt := lt.
-Definition le := le.
-Definition recursion : forall A : Set, A -> (N -> A -> A) -> N -> A :=
-  fun A : Set => nat_rec (fun _ => A).
-Implicit Arguments recursion [A].
-
-Theorem E_equiv : equiv nat E.
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ := nat.
+Definition NZE := (@eq nat).
+Definition NZ0 := 0.
+Definition NZsucc := S.
+Definition NZpred := pred.
+Definition NZplus := plus.
+Definition NZminus := minus.
+Definition NZtimes := mult.
+
+Theorem NZE_equiv : equiv nat NZE.
 Proof (eq_equiv nat).
 
-Add Relation nat E
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
+Add Relation nat NZE
+ reflexivity proved by (proj1 NZE_equiv)
+ symmetry proved by (proj2 (proj2 NZE_equiv))
+ transitivity proved by (proj1 (proj2 NZE_equiv))
+as NZE_rel.
 
-(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat E"
+(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZE"
 then the theorem generated for succ_wd below is forall x, succ x = succ x,
 which does not match the axioms in NAxiomsSig *)
 
-Add Morphism S with signature E ==> E as succ_wd.
+Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism P with signature E ==> E as pred_wd.
+Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism times with signature E ==> E ==> E as times_wd.
+Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
 Proof.
 congruence.
 Qed.
 
-Add Morphism lt with signature E ==> E ==> iff as lt_wd.
-Proof.
-unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism le with signature E ==> E ==> iff as le_wd.
-Proof.
-unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Theorem induction :
+Theorem NZinduction :
   forall A : nat -> Prop, predicate_wd (@eq nat) A ->
-    A 0 -> (forall n : nat, A n -> A (S n)) -> forall n : nat, A n.
+    A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
 Proof.
-intros; now apply nat_ind.
+intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
 Qed.
 
-Theorem pred_0 : pred 0 = 0.
-Proof.
-reflexivity.
-Qed.
-
-Theorem pred_succ : forall n : nat, pred (S n) = n.
+Theorem NZpred_succ : forall n : nat, pred (S n) = n.
 Proof.
 reflexivity.
 Qed.
 
-Theorem plus_0_l : forall n : nat, 0 + n = n.
+Theorem NZplus_0_l : forall n : nat, 0 + n = n.
 Proof.
 reflexivity.
 Qed.
 
-Theorem plus_succ_l : forall n m : nat, (S n) + m = S (n + m).
+Theorem NZplus_succ_l : forall n m : nat, (S n) + m = S (n + m).
 Proof.
 reflexivity.
 Qed.
 
-Theorem minus_0_r : forall n : nat, n - 0 = n.
+Theorem NZminus_0_r : forall n : nat, n - 0 = n.
 Proof.
 intro n; now destruct n.
 Qed.
 
-Theorem minus_succ_r : forall n m : nat, n - (S m) = pred (n - m).
+Theorem NZminus_succ_r : forall n m : nat, n - (S m) = pred (n - m).
 Proof.
-intros n m; induction n m using nat_double_ind; simpl; auto. apply minus_0_r.
+intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r.
 Qed.
 
-Theorem times_0_r : forall n : nat, n * 0 = 0.
+Theorem NZtimes_0_r : forall n : nat, n * 0 = 0.
 Proof.
 exact mult_0_r.
 Qed.
 
-Theorem times_succ_r : forall n m : nat, n * (S m) = n * m + n.
+Theorem NZtimes_succ_r : forall n m : nat, n * (S m) = n * m + n.
 Proof.
 intros n m; symmetry; apply mult_n_Sm.
 Qed.
 
-Theorem le_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m.
-Proof.
-intros n m; split.
-apply le_lt_or_eq.
-intro H; destruct H as [H | H].
-now apply lt_le_weak. rewrite H; apply le_refl.
-Qed.
-
-Theorem nlt_0_r : forall n : nat, ~ (n < 0).
-Proof.
-exact lt_n_O.
-Qed.
-
-Theorem lt_succ_le : forall n m : nat, n < S m <-> n <= m.
-Proof.
-intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm].
-Qed.
-
-Theorem recursion_wd : forall (A : Set) (EA : relation A),
-  forall a a' : A, EA a a' ->
-    forall f f' : N -> A -> A, eq_fun2 (@eq nat) EA EA f f' ->
-      forall n n' : N, n = n' ->
-        EA (recursion a f n) (recursion a' f' n').
-Proof.
-unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
-Qed.
-
-Theorem recursion_0 :
-  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
-Proof.
-reflexivity.
-Qed.
-
-Theorem recursion_succ :
-  forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
-    EA a a -> fun2_wd (@eq nat) EA EA f ->
-      forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
-Proof.
-unfold eq_fun2; induction n; simpl; auto.
-Qed.
-
-End NPeanoAxiomsMod.
-
-(* Now we apply the largest property functor *)
-
-Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod.
-
-(*
-
-Theorem succ_wd : fun_wd (@eq nat) (@eq nat) S.
-Proof.
-congruence.
-Qed.
-
-Theorem succ_inj : forall n1 n2 : nat, S n1 = S n2 -> n1 = n2.
-Proof.
-intros n1 n2 H; now simplify_eq H.
-Qed.
-
-Theorem succ_neq_0 : forall n : nat, S n <> 0.
-Proof.
-intros n H; simplify_eq H.
-Qed.
-
-
-Definition N := nat.
-Definition E := (@eq nat).
-Definition O := 0.
-Definition S := S.
-
-End NPeanoBaseMod.
-
-Module NPeanoPlusMod <: NPlusSig.
-Module NBaseMod := NPeanoBaseMod.
-
-Theorem plus_wd : fun2_wd (@eq nat) (@eq nat) (@eq nat) plus.
-Proof.
-congruence.
-Qed.
-
-Theorem plus_0_l : forall n, 0 + n = n.
-Proof.
-reflexivity.
-Qed.
-
-Theorem plus_succ_l : forall n m, (S n) + m = S (n + m).
-Proof.
-reflexivity.
-Qed.
-
-Definition plus := plus.
-
-End NPeanoPlusMod.
-
-Module Export NPeanoBasePropMod := NBasePropFunct NPeanoBaseMod.
-Module Export NPeanoPlusPropMod := NPlusPropFunct NPeanoPlusMod.
-
-
-Module Export NPeanoDepRec <: NDepRecSignature.
-Module Import NDomainModule := NPeanoDomain.
-Module Import NBaseMod := PeanoNat.
-
-Definition dep_recursion := nat_rec.
-
-Theorem 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.
-Proof.
-reflexivity.
-Qed.
-
-Theorem 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).
-Proof.
-reflexivity.
-Qed.
-
-End NPeanoDepRec.
-
-Module Export NPeanoOrder <: NOrderSig.
-Module Import NBaseMod := PeanoNat.
-
-Definition lt := lt.
-Definition le := le.
-
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
-Proof.
-unfold E, eq_bool; congruence.
-Qed.
-
-Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
-Proof.
-unfold E, eq_bool; congruence.
-Qed.
-
-(* It would be easier to prove the boolean lemma first because
-|| is simplified by simpl unlike \/ *)
-Lemma le_lt_bool : forall x y, le x y = (lt x y) || (e x y).
-Proof.
-induction x as [| x IH]; destruct y; simpl; (reflexivity || apply IH).
-Qed.
-
-Theorem le_lt : forall x y, le x y <-> lt x y \/ x = y.
-Proof.
-intros; rewrite E_equiv_e; rewrite <- eq_true_or;
-rewrite <- eq_true_iff; apply le_lt_bool.
-Qed.
+End NZAxiomsMod.
 
-Theorem lt_0 : forall x, ~ (lt x 0).
-Proof.
-destruct x as [|x]; simpl; now intro.
-Qed.
+Definition NZlt := lt.
+Definition NZle := le.
 
-Lemma lt_succ_bool : forall x y, lt x (S y) = le x y.
+Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
 Proof.
-unfold lt, le; induction x as [| x IH]; destruct y as [| y];
-simpl; try reflexivity.
-destruct x; now simpl.
-apply IH.
+unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
 Qed.
 
-Theorem lt_succ : forall x y, lt x (S y) <-> le x y.
+Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
 Proof.
-intros; rewrite <- eq_true_iff; apply lt_succ_bool.
+unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
 Qed.
 
-End NPeanoOrder.
-
-Module Export NPeanoTimes <: NTimesSig.
-Module Import NPlusMod := NPeanoPlus.
-
-Definition times := mult.
-
-Add Morphism times with signature E ==> E ==> E as times_wd.
+Theorem NZle_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m.
 Proof.
-unfold E; congruence.
+intros n m; split.
+apply le_lt_or_eq.
+intro H; destruct H as [H | H].
+now apply lt_le_weak. rewrite H; apply le_refl.
 Qed.
 
-Theorem times_0_r : forall n, n * 0 = 0.
+Theorem NZlt_irrefl : forall n : nat, ~ (n < n).
 Proof.
-auto.
+exact lt_irrefl.
 Qed.
 
-Theorem times_succ_r : forall n m, n * (S m) = n * m + n.
+Theorem NZlt_succ_le : forall n m : nat, n < S m <-> n <= m.
 Proof.
-auto.
+intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm].
 Qed.
 
-End NPeanoTimes.
+End NZOrdAxiomsMod.
 
-Module Export NPeanoPred <: NPredSignature.
-Module Export NBaseMod := PeanoNat.
-
-Definition P (n : nat) :=
-match n with
-| 0 => 0
-| S n' => n'
-end.
+Definition recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A :=
+  fun A : Set => nat_rec (fun _ => A).
+Implicit Arguments recursion [A].
 
-Add Morphism P with signature E ==> E as pred_wd.
+Theorem succ_neq_0 : forall n : nat, S n <> 0.
 Proof.
-unfold E; congruence.
+intros; discriminate.
 Qed.
 
-Theorem pred_0 : P 0 = 0.
+Theorem pred_0 : pred 0 = 0.
 Proof.
 reflexivity.
 Qed.
 
-Theorem pred_succ : forall n, P (S n) = n.
-Proof.
-now intro.
-Qed.
-
-End NPeanoPred.
-
-Module Export NPeanoMinus <: NMinusSignature.
-Module Import NPredModule := NPeanoPred.
-
-Definition minus := minus.
-
-Add Morphism minus with signature E ==> E ==> E as minus_wd.
-Proof.
-unfold E; congruence.
-Qed.
-
-Theorem minus_0_r : forall n, n - 0 = n.
-Proof.
-now destruct n.
-Qed.
-
-Theorem minus_succ_r : forall n m, n - (S m) = P (n - m).
-Proof.
-induction n as [| n IH]; simpl.
-now intro.
-destruct m; simpl; [apply minus_0_r | apply IH].
-Qed.
-
-End NPeanoMinus.
-
-(* Obtaining properties for +, *, <, and their combinations *)
-
-Module Export NPeanoTimesOrderProperties := NTimesOrderProperties NPeanoTimes NPeanoOrder.
-Module Export NPeanoDepRecTimesProperties :=
-  NDepRecTimesProperties NPeanoDepRec NPeanoTimes.
-Module Export NPeanoMinusProperties :=
-  NMinusProperties NPeanoMinus NPeanoPlus NPeanoOrder.
-
-Module MiscFunctModule := MiscFunctFunctor PeanoNat.
-(* The instruction above adds about 0.5M to the size of the .vo file !!! *)
-
-Theorem E_equiv_e : forall x y : N, E x y <-> e x y.
-Proof.
-induction x; destruct y; simpl; try now split; intro.
-rewrite <- IHx; split; intro H; [now injection H | now rewrite H].
-Qed.
-
-Definition recursion := fun A : Set => nat_rec (fun _ => A).
-Implicit Arguments recursion [A].
-
-Theorem recursion_wd :
-forall (A : Set) (EA : relation A),
+Theorem 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' ->
-      forall x x' : N, x = x' ->
-        EA (recursion a f x) (recursion a' f' x').
+    forall f f' : nat -> A -> A, eq_fun2 (@eq nat) EA EA f f' ->
+      forall n n' : nat, n = n' ->
+        EA (recursion a f n) (recursion a' f' n').
 Proof.
-unfold fun2_wd, E.
-intros A EA a a' Eaa' f f' Eff'.
-induction x as [| n IH]; intros x' H; rewrite <- H; simpl.
-assumption.
-apply Eff'; [reflexivity | now apply IH].
+unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
 Qed.
 
 Theorem recursion_0 :
-  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f O = a.
+  forall (A : Set) (a : A) (f : nat -> A -> A), recursion a f 0 = a.
 Proof.
 reflexivity.
 Qed.
 
 Theorem 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) (EA : relation A) (a : A) (f : nat -> A -> A),
+    EA a a -> fun2_wd (@eq nat) EA EA f ->
+      forall n : nat, EA (recursion a f (S n)) (f n (recursion a f n)).
 Proof.
-intros A EA a f EAaa f_wd. unfold fun2_wd, E in *.
-induction n; simpl; now apply f_wd.
+unfold eq_fun2; induction n; simpl; auto.
 Qed.
 
-(*Lemma e_implies_E : forall n m, e n m = true -> n = m.
-Proof.
-intros n m H; rewrite <- eq_true_unfold_pos in H;
-now apply <- E_equiv_e.
-Qed.
+End NPeanoAxiomsMod.
 
-Add Ring SR : semi_ring (decidable e_implies_E).
+(* Now we apply the largest property functor *)
 
-Goal forall x y : nat, x + y = y + x. intros. ring.*)
-*)
+Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod.
 
 
 (*