Added the proof (in Numbers/Integers/TreeMod) that tree-like representation of integers due to Gregoire and Théry satisfies the axioms of integers without order. This refers to integers modulo n, i.e., those that fit trees of certain size, not to BigZ.

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

7 files changed, 216 insertions, 455 deletions

diff --git a/theories/Numbers/Integer/BigInts/EZBase.v b/theories/Numbers/Integer/BigInts/EZBase.v
deleted file mode 100644
index a1e52a2024..0000000000
--- a/theories/Numbers/Integer/BigInts/EZBase.v
+++ /dev/null
@@ -1,161 +0,0 @@
-Require Export ZBase.
-(*Require Import BigN.*)
-Require Import NMake.
-Require Import ZnZ.
-Require Import Basic_type.
-Require Import ZAux.
-Require Import Zeqmod.
-Require Import ZArith.
-
-Module EZBaseMod (Import EffIntsMod : W0Type) <: ZBaseSig.
-Open Local Scope Z_scope.
-
-Definition Z := EffIntsMod.w.
-
-Definition w_op := EffIntsMod.w_op.
-Definition w_spec := EffIntsMod.w_spec.
-Definition to_Z := w_op.(znz_to_Z).
-Definition of_Z := znz_of_Z w_op.
-Definition wB := base w_op.(znz_digits).
-
-Theorem Zpow_gt_1 : forall n m : BinInt.Z, 0 < n -> 1 < m -> 1 < m ^ n.
-Proof.
-intros n m H1 H2.
-replace 1 with (m ^ 0) by apply Zpower_exp_0.
-apply Zpower_lt_monotone; auto with zarith.
-Qed.
-
-Theorem wB_gt_1 : 1 < wB.
-Proof.
-unfold wB, base. apply Zpow_gt_1; unfold Zlt; auto with zarith.
-Qed.
-
-Theorem wB_gt_0 : 0 < wB.
-Proof.
-pose proof wB_gt_1; auto with zarith.
-Qed.
-
-Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).
-
-Theorem to_Z_spec : forall x : Z, 0 <= [|x|] < wB.
-Proof w_spec.(spec_to_Z).
-
-Definition ZE (n m : Z) := [|n|] = [|m|].
-
-Notation "x == y"  := (ZE x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ ZE x y) (at level 70) : IntScope.
-Open Local Scope IntScope.
-
-Theorem ZE_equiv : equiv Z ZE.
-Proof.
-unfold equiv, reflexive, symmetric, transitive, ZE; repeat split; intros; auto.
-now transitivity [|y|].
-Qed.
-
-Add Relation Z ZE
- reflexivity proved by (proj1 ZE_equiv)
- symmetry proved by (proj2 (proj2 ZE_equiv))
- transitivity proved by (proj1 (proj2 ZE_equiv))
-as ZE_rel.
-
-Definition Z0 := w_op.(znz_0).
-Definition Zsucc := w_op.(znz_succ).
-
-Notation "0" := Z0 : IntScope.
-Notation "'S'" := Zsucc : IntScope.
-Notation "1" := (S 0) : IntScope.
-
-Theorem Zsucc_spec : forall n : Z, [|S n|] = ([|n|] + 1) mod wB.
-Proof w_spec.(spec_succ).
-
-Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
-Proof.
-unfold ZE; intros n m H. do 2 rewrite Zsucc_spec. now rewrite H.
-Qed.
-
-Theorem Zsucc_inj : forall x y : Z, S x == S y -> x == y.
-Proof.
-intros x y H; unfold ZE in *; do 2 rewrite Zsucc_spec in H.
-apply <- Zplus_eqmod_compat_r in H.
-do 2 rewrite Zmod_def_small in H; now try apply to_Z_spec.
-apply wB_gt_0.
-Qed.
-
-Lemma of_Z_0 : of_Z 0 == Z0.
-Proof.
-unfold ZE, to_Z, of_Z. rewrite znz_of_Z_correct.
-symmetry; apply w_spec.(spec_0).
-exact w_spec. split; [auto with zarith |apply wB_gt_0].
-Qed.
-
-Section Induction.
-
-Variable A : Z -> Prop.
-Hypothesis A_wd : predicate_wd ZE A.
-Hypothesis A0 : A 0.
-Hypothesis AS : forall n : Z, A n <-> A (S n). (* In fact, it's enought to have only -> *)
-
-Add Morphism A with signature ZE ==> iff as A_morph.
-Proof A_wd.
-
-Let B (n : BinInt.Z) := A (of_Z n).
-
-Lemma B0 : B 0.
-Proof.
-unfold B. now rewrite of_Z_0.
-Qed.
-
-Lemma BS : forall n : BinInt.Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
-Proof.
-intros n H1 H2 H3.
-unfold B in *. apply -> AS in H3.
-setoid_replace (of_Z (n + 1)) with (S (of_Z n)) using relation ZE. assumption.
-unfold ZE. rewrite Zsucc_spec.
-unfold to_Z, of_Z. rewrite znz_of_Z_correct. rewrite znz_of_Z_correct.
-symmetry; apply Zmod_def_small; auto with zarith.
-exact w_spec.
-unfold wB in *; auto with zarith.
-exact w_spec.
-unfold wB in *; auto with zarith.
-Qed.
-
-Lemma Zbounded_induction :
-  (forall Q : BinInt.Z -> Prop, forall b : BinInt.Z,
-    Q 0 ->
-    (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
-      forall n, 0 <= n -> n < b -> Q n)%Z.
-Proof.
-intros Q b Q0 QS.
-set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)).
-assert (H : forall n, 0 <= n -> Q' n).
-apply natlike_rec2; unfold Q'.
-destruct (Zle_or_lt b 0) as [H | H]. now right. left; now split.
-intros n H IH. destruct IH as [[IH1 IH2] | IH].
-destruct (Zle_or_lt (b - 1) n) as [H1 | H1].
-right; auto with zarith.
-left. split; [auto with zarith | now apply (QS n)].
-right; auto with zarith.
-unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3].
-assumption. apply Zle_not_lt in H3. false_hyp H2 H3.
-Qed.
-
-Lemma B_holds : forall n : BinInt.Z, 0 <= n < wB -> B n.
-Proof.
-intros n [H1 H2].
-apply Zbounded_induction with wB.
-apply B0. apply BS. assumption. assumption.
-Qed.
-
-Theorem Zinduction : forall n : Z, A n.
-Proof.
-intro n. setoid_replace n with (of_Z (to_Z n)) using relation ZE.
-apply B_holds. apply to_Z_spec.
-unfold ZE, to_Z, of_Z; rewrite znz_of_Z_correct.
-reflexivity.
-exact w_spec.
-apply to_Z_spec.
-Qed.
-
-End Induction.
-
-End EZBaseMod.
diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v
deleted file mode 100644
index b31dcdf9df..0000000000
--- a/theories/Numbers/Integer/BigInts/Zeqmod.v
+++ /dev/null
@@ -1,42 +0,0 @@
-Require Import ZArith.
-Require Import ZAux.
-
-Open Local Scope Z_scope.
-Notation "x == y '[' 'mod' z ']'" := ((x mod z) = (y mod z))
-  (at level 70, no associativity) : Z_scope.
-
-Theorem Zeqmod_refl : forall p n : Z, n == n [mod p].
-Proof.
-reflexivity.
-Qed.
-
-Theorem Zeqmod_symm : forall p n m : Z, n == m [mod p] -> m == n [mod p].
-Proof.
-now symmetry.
-Qed.
-
-Theorem Zeqmod_trans :
-  forall p n m k : Z, n == m [mod p] -> m == k [mod p] -> n == k [mod p].
-Proof.
-intros p n m k H1 H2; now transitivity (m mod p).
-Qed.
-
-Theorem Zplus_eqmod_compat_l :
-  forall p n m k : Z, 0 < p -> (n == m [mod p] <-> k + n == k + m [mod p]).
-intros p n m k H1.
-assert (LR : forall n' m' k' : Z, n' == m' [mod p] -> k' + n' == k' + m' [mod p]).
-intros n' m' k' H2.
-pattern ((k' + n') mod p); rewrite Zmod_plus; [| assumption].
-pattern ((k' + m') mod p); rewrite Zmod_plus; [| assumption].
-rewrite H2. apply Zeqmod_refl.
-split; [apply LR |].
-intro H2. apply (LR (k + n) (k + m) (-k)) in H2.
-do 2 rewrite Zplus_assoc in H2. rewrite Zplus_opp_l in H2.
-now do 2 rewrite Zplus_0_l in H2.
-Qed.
-
-Theorem Zplus_eqmod_compat_r :
-  forall p n m k : Z, 0 < p -> (n == m [mod p] <-> n + k == m + k [mod p]).
-intros p n m k; rewrite (Zplus_comm n k); rewrite (Zplus_comm m k);
-apply Zplus_eqmod_compat_l.
-Qed.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 41fc7e75ee..5c8b5890d5 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -25,7 +25,6 @@ In that case, we could get rid of setoids as well as arrive at integers as
 signed natural numbers. *)
 Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)).
 Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)).
-Definition NZuminus (n : Z) := (snd n, fst n).
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
 Definition NZtimes (n m : Z) :=
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
deleted file mode 100644
index dc258f873f..0000000000
--- a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
+++ /dev/null
@@ -1,112 +0,0 @@
-Require Import NPlusOrder.
-Require Export ZPlusOrder.
-Require Export ZPairsPlus.
-
-Module NatPairsOrder (Import NPlusMod : NPlusSig)
-                     (Import NOrderModule : NOrderSig
-                        with Module NBaseMod := NPlusMod.NBaseMod) <: ZOrderSignature.
-Module Import NPlusOrderPropertiesModule :=
-  NPlusOrderProperties NPlusMod NOrderModule.
-Module Export ZBaseMod := NatPairsInt NPlusMod.
-Open Local Scope NatScope.
-
-Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1).
-Definition le (p1 p2 : Z) := (fst p1) + (snd p2) <= (fst p2) + (snd p1).
-
-Notation "x < y" := (lt x y) : IntScope.
-Notation "x <= y" := (le x y) : IntScope.
-
-Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
-Proof.
-unfold lt, E; intros x1 y1 H1 x2 y2 H2; simpl.
-rewrite eq_true_iff; split; intro H.
-stepr (snd y1 + fst y2) by apply plus_comm.
-apply (plus_lt_repl_pair (fst x1) (snd x1)); [| assumption].
-stepl (snd y2 + fst x1) by apply plus_comm.
-stepr (fst y2 + snd x1) by apply plus_comm.
-apply (plus_lt_repl_pair (snd x2) (fst x2)).
-now stepl (fst x1 + snd x2) by apply plus_comm.
-stepl (fst y2 + snd x2) by apply plus_comm. now stepr (fst x2 + snd y2) by apply plus_comm.
-stepr (snd x1 + fst x2) by apply plus_comm.
-apply (plus_lt_repl_pair (fst y1) (snd y1)); [| now symmetry].
-stepl (snd x2 + fst y1) by apply plus_comm.
-stepr (fst x2 + snd y1) by apply plus_comm.
-apply (plus_lt_repl_pair (snd y2) (fst y2)).
-now stepl (fst y1 + snd y2) by apply plus_comm.
-stepl (fst x2 + snd y2) by apply plus_comm. now stepr (fst y2 + snd x2) by apply plus_comm.
-Qed.
-
-(* Below is a very long explanation why it would be useful to be
-able to use the fold tactic in hypotheses.
-We will prove the following statement not from scratch, like lt_wd,
-but expanding <= to < and == and then using lt_wd. The theorem we need
-to prove is (x1 <= x2) = (y1 <= y2) for all x1 == y1 and x2 == y2 : Z.
-To be able to express <= through < and ==, we need to expand <=%Int to
-<=%Nat, since we have not proved yet the properties of <=%Int. But
-then it would be convenient to fold back equalities from
-(fst x1 + snd x2 == fst x2 + snd x1)%Nat to (x1 == x2)%Int.
-The reason is that we will need to show that (x1 == x2)%Int <->
-(y1 == y2)%Int from (x1 == x2)%Int and (y1 == y2)%Int. If we fold
-equalities back to Int, then we could do simple rewriting, since we have
-already showed that ==%Int is an equivalence relation. On the other hand,
-if we leave equalities expanded to Nat, we will have to apply the
-transitivity of ==%Int by hand. *)
-
-Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
-Proof.
-unfold le, E; intros x1 y1 H1 x2 y2 H2; simpl.
-rewrite eq_true_iff. do 2 rewrite le_lt.
-pose proof (lt_wd x1 y1 H1 x2 y2 H2) as H; unfold lt in H; rewrite H; clear H.
-(* This is a remark about an extra level of definitions created by
-"with Module NBaseMod := NPlusMod.NBaseMod" constraint in the beginning
-of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out
-that it expand to (NPlusMod.NBaseMod.NDomainModule.E ... ...), since
-NPlusMod was imported first. On the other hand, the goal uses
-NOrderModule.NBaseMod.NDomainModule.E, or just NDomainModule.E, since le_lt
-theorem was proved in NOrderDomain module. (E without qualifiers refers to
-ZDomainModule.E.) Therefore, we issue the "replace" command. It would be nicer,
-though, if the constraint "with Module NBaseMod := NPlusMod.NBaseMod" in the
-declaration of this functor would not create an extra level of definitions
-and there would be only one NDomainModule.E. *)
-replace NDomainModule.E with NPlusMod.NBaseMod.NDomainModule.E by reflexivity.
-fold (x1 == x2)%Int. fold (y1 == y2)%Int.
-assert (H1' : (x1 == y1)%Int); [exact H1 |].
-(* We do this instead of "fold (x1 == y1)%Int in H1" *)
-assert (H2' : (x2 == y2)%Int); [exact H2 |].
-rewrite H1'; rewrite H2'. reflexivity.
-Qed.
-
-Open Local Scope IntScope.
-
-Theorem le_lt : forall n m : Z, n <= m <-> n < m \/ n == m.
-Proof.
-intros n m; unfold lt, le, E; simpl. apply le_lt. (* refers to NOrderModule.le_lt *)
-Qed.
-
-Theorem lt_irr : forall n : Z, ~ (n < n).
-Proof.
-intros n; unfold lt, E; simpl. apply lt_irr.
-(* refers to NPlusOrderPropertiesModule.NOrderPropFunctModule.lt_irr *)
-Qed.
-
-Theorem lt_succ : forall n m, n < (S m) <-> n <= m.
-Proof.
-intros n m; unfold lt, le, E; simpl. rewrite plus_succ_l; apply lt_succ.
-Qed.
-
-End NatPairsOrder.
-
-(* Since to define the order on integers we need both plus and order
-on natural numbers, we can export the properties of plus and order together *)
-(*Module NatPairsPlusOrderProperties (NPlusMod : NPlusSig)
-                                   (NOrderModule : NOrderSig
-                                     with Module NBaseMod := NPlusMod.NBaseMod).
-Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
-Module Export NatPairsOrderModule := NatPairsOrder NPlusMod NOrderModule.
-Module Export NatPairsPlusOrderPropertiesModule :=
-  ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule.
-End NatPairsPlusOrderProperties.*)
-(* We cannot prove to Coq that NatPairsPlusModule.ZBaseMod and
-NatPairsOrderModule.ZBaseMod are the same *)
-
-
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
deleted file mode 100644
index 2e658c181f..0000000000
--- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
+++ /dev/null
@@ -1,83 +0,0 @@
-Require Import NPlus.
-Require Export ZPlus.
-Require Export ZPairsAxioms.
-
-Module NatPairsPlus (Import NPlusMod : NPlusSig) <: ZPlusSignature.
-Module Export ZBaseMod := NatPairsInt NPlusMod.
-Open Local Scope NatScope.
-
-Definition plus (x y : Z) := ((fst x) + (fst y), (snd x) + (snd y)).
-Definition minus (x y : Z) := ((fst x) + (snd y), (snd x) + (fst y)).
-Definition uminus (x : Z) := (snd x, fst x).
-(* Unfortunately, the elements of pair keep increasing, even during subtraction *)
-
-Notation "x + y" := (plus x y) : IntScope.
-Notation "x - y" := (minus x y) : IntScope.
-Notation "- x" := (uminus x) : IntScope.
-
-(* Below, we need to rewrite subtems that have several occurrences.
-Since with the currect setoid_rewrite we cannot point an accurrence
-using pattern, we use symmetry tactic to make a particular occurrence
-the leftmost, since that is what rewrite will use. *)
-Add Morphism plus with signature E ==> E ==> E as plus_wd.
-Proof.
-unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl.
-pose proof (plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
-                    (fst x2 + snd y2) (fst y2 + snd x2) H2) as H.
-rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1.
-Qed.
-
-Add Morphism minus with signature E ==> E ==> E as minus_wd.
-Proof.
-unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl.
-rewrite plus_comm in H2. symmetry in H2; rewrite plus_comm in H2.
-pose proof (NPlusMod.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
-                                (snd x2 + fst y2) (snd y2 + fst x2) H2) as H.
-rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1.
-Qed.
-
-Add Morphism uminus with signature E ==> E as uminus_wd.
-Proof.
-unfold E, plus; intros x y H; simpl.
-rewrite plus_comm. symmetry. now rewrite plus_comm.
-Qed.
-
-Open Local Scope IntScope.
-
-Theorem plus_0 : forall n, 0 + n == n.
-Proof.
-intro n; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_0_l.
-Qed.
-
-Theorem plus_succ : forall n m, (S n) + m == S (n + m).
-Proof.
-intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_succ_l.
-Qed.
-
-Theorem minus_0 : forall n, n - 0 == n.
-Proof.
-intro n; unfold minus, E; simpl. now do 2 rewrite plus_0_r.
-Qed.
-
-Theorem minus_succ : forall n m, n - (S m) == P (n - m).
-Proof.
-intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_succ_r.
-Qed.
-
-Theorem uminus_0 : - 0 == 0.
-Proof.
-unfold uminus, E; simpl. now rewrite plus_0_l.
-Qed.
-
-Theorem uminus_succ : forall n, - (S n) == P (- n).
-Proof.
-reflexivity.
-Qed.
-
-End NatPairsPlus.
-
-Module NatPairsPlusProperties (NPlusMod : NPlusSig).
-Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
-Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule.
-End NatPairsPlusProperties.
-
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
deleted file mode 100644
index 553c6df22f..0000000000
--- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
+++ /dev/null
@@ -1,56 +0,0 @@
-Require Import Ring.
-Require Import NTimes.
-Require Export ZTimes.
-Require Export ZPairsPlus.
-
-Module NatPairsTimes (Import NTimesMod : NTimesSig) <: ZTimesSignature.
-Module Export ZPlusModule := NatPairsPlus NTimesMod.NPlusMod. (* "NTimesMod." is optional *)
-Module Import NTimesPropertiesModule := NTimesPropFunct NTimesMod.
-Open Local Scope NatScope.
-
-Definition times (n m : Z) :=
-  ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
-
-Notation "x * y" := (times x y) : IntScope.
-
-Add Morphism times with signature E ==> E ==> E as times_wd.
-Proof.
-unfold times, E; intros x1 y1 H1 x2 y2 H2; simpl.
-stepl_ring (fst x1 * fst x2 + (snd x1 * snd x2 + fst y1 * snd y2 + snd y1 * fst y2)).
-stepr_ring (fst x1 * snd x2 + (fst y1 * fst y2 + snd y1 * snd y2 + snd x1 * fst x2)).
-apply plus_times_repl_pair with (n := fst y2) (m := snd y2); [| now idtac].
-stepl_ring (snd x1 * snd x2 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
-stepr_ring (snd x1 * fst x2 + (fst x1 * snd y2 + fst y1 * fst y2 + snd y1 * snd y2)).
-apply plus_times_repl_pair with (n := snd y2) (m := fst y2);
-  [| rewrite plus_comm; symmetry; now rewrite plus_comm].
-stepl_ring (snd y2 * snd x1 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
-stepr_ring (snd y2 * fst x1 + (snd x1 * fst y2 + fst y1 * fst y2 + snd y1 * snd y2)).
-apply plus_times_repl_pair with (n := snd y1) (m := fst y1);
-  [| rewrite plus_comm; symmetry; now rewrite plus_comm].
-stepl_ring (fst y2 * fst x1 + (snd y2 * snd y1 + fst y1 * snd y2 + snd y1 * fst y2)).
-stepr_ring (fst y2 * snd x1 + (snd y2 * fst y1 + fst y1 * fst y2 + snd y1 * snd y2)).
-apply plus_times_repl_pair with (n := fst y1) (m := snd y1); [| now idtac].
-ring.
-Qed.
-
-Open Local Scope IntScope.
-
-Theorem times_0 : forall n, n * 0 == 0.
-Proof.
-intro n; unfold times, E; simpl.
-repeat rewrite times_0_r. now rewrite plus_assoc.
-Qed.
-
-Theorem times_succ : forall n m, n * (S m) == n * m + n.
-Proof.
-intros n m; unfold times, S, E; simpl.
-do 2 rewrite times_succ_r. ring.
-Qed.
-
-End NatPairsTimes.
-
-Module NatPairsTimesProperties (NTimesMod : NTimesSig).
-Module Export NatPairsTimesModule := NatPairsTimes NTimesMod.
-Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule.
-End NatPairsTimesProperties.
-
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
new file mode 100644
index 0000000000..7479868e9d
--- /dev/null
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -0,0 +1,216 @@
+Require Export NZAxioms.
+Require Import NMake. (* contains W0Type *)
+Require Import ZnZ.
+Require Import Basic_type. (* contais base *)
+Require Import ZAux.
+
+Module NZBigIntsAxiomsMod (Import BoundedIntsMod : W0Type) <: NZAxiomsSig.
+
+Open Local Scope Z_scope.
+
+Definition NZ := w.
+
+Definition NZ_to_Z : NZ -> Z := znz_to_Z w_op.
+Definition Z_to_NZ : Z -> NZ := znz_of_Z w_op.
+Notation Local wB := (base w_op.(znz_digits)).
+
+Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
+
+Definition NZE (n m : NZ) := [| n |] = [| m |].
+Definition NZ0 := w_op.(znz_0).
+Definition NZsucc := w_op.(znz_succ).
+Definition NZpred := w_op.(znz_pred).
+Definition NZplus := w_op.(znz_add).
+Definition NZminus := w_op.(znz_sub).
+Definition NZtimes := w_op.(znz_mul).
+
+Theorem NZE_equiv : equiv NZ NZE.
+Proof.
+unfold equiv, reflexive, symmetric, transitive, NZE; repeat split; intros; auto.
+now transitivity [| y |].
+Qed.
+
+Add Relation NZ 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 NZsucc with signature NZE ==> NZE as NZsucc_wd.
+Proof.
+unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H.
+Qed.
+
+Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
+Proof.
+unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
+Qed.
+
+Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
+Proof.
+unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
+now rewrite H1, H2.
+Qed.
+
+Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
+Proof.
+unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
+now rewrite H1, H2.
+Qed.
+
+Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
+Proof.
+unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul).
+now rewrite H1, H2.
+Qed.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with NZ.
+Open Local Scope IntScope.
+Notation "x == y"  := (NZE x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope.
+Notation "0" := NZ0 : IntScope.
+Notation "'S'" := NZsucc : IntScope.
+Notation "'P'" := NZpred : IntScope.
+(*Notation "1" := (S 0) : IntScope.*)
+Notation "x + y" := (NZplus x y) : IntScope.
+Notation "x - y" := (NZminus x y) : IntScope.
+Notation "x * y" := (NZtimes x y) : IntScope.
+
+Theorem gt_wB_1 : 1 < wB.
+Proof.
+unfold base. apply Zgt_pow_1; unfold Zlt; auto with zarith.
+Qed.
+
+Theorem gt_wB_0 : 0 < wB.
+Proof.
+pose proof gt_wB_1; auto with zarith.
+Qed.
+
+Lemma NZsucc_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
+Proof.
+intro n.
+pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zmod_plus; [ | apply gt_wB_0].
+reflexivity.
+now rewrite Zmod_def_small; [ | split; [auto with zarith | apply gt_wB_1]].
+Qed.
+
+Lemma NZpred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
+Proof.
+intro n.
+pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zmod_minus; [ | apply gt_wB_0].
+reflexivity.
+now rewrite Zmod_def_small; [ | split; [auto with zarith | apply gt_wB_1]].
+Qed.
+
+Lemma NZ_to_Z_mod : forall n : NZ, [| n |] mod wB = [| n |].
+Proof.
+intro n; rewrite Zmod_def_small. reflexivity. apply w_spec.(spec_to_Z).
+Qed.
+
+Theorem NZpred_succ : forall n : NZ, P (S n) == n.
+Proof.
+intro n; unfold NZsucc, NZpred, NZE. rewrite w_spec.(spec_pred), w_spec.(spec_succ).
+rewrite <- NZpred_mod_wB.
+replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod.
+Qed.
+
+Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int.
+Proof.
+unfold NZE, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct.
+symmetry; apply w_spec.(spec_0).
+exact w_spec. split; [auto with zarith |apply gt_wB_0].
+Qed.
+
+Section Induction.
+
+Variable A : NZ -> Prop.
+Hypothesis A_wd : predicate_wd NZE A.
+Hypothesis A0 : A 0.
+Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *)
+
+Add Morphism A with signature NZE ==> iff as A_morph.
+Proof A_wd.
+
+Let B (n : Z) := A (Z_to_NZ n).
+
+Lemma B0 : B 0.
+Proof.
+unfold B. now rewrite Z_to_NZ_0.
+Qed.
+
+Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
+Proof.
+intros n H1 H2 H3.
+unfold B in *. apply -> AS in H3.
+setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZE. assumption.
+unfold NZE. rewrite w_spec.(spec_succ).
+unfold NZ_to_Z, Z_to_NZ.
+do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]).
+symmetry; apply Zmod_def_small; auto with zarith.
+Qed.
+
+Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.
+Proof.
+intros n [H1 H2].
+apply Zbounded_induction with wB.
+apply B0. apply BS. assumption. assumption.
+Qed.
+
+Theorem NZinduction : forall n : NZ, A n.
+Proof.
+intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZE.
+apply B_holds. apply w_spec.(spec_to_Z).
+unfold NZE, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
+reflexivity.
+exact w_spec.
+apply w_spec.(spec_to_Z).
+Qed.
+
+End Induction.
+
+Theorem NZplus_0_l : forall n : NZ, 0 + n == n.
+Proof.
+intro n; unfold NZplus, NZ0, NZE. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
+rewrite Zplus_0_l. rewrite Zmod_def_small; [reflexivity | apply w_spec.(spec_to_Z)].
+Qed.
+
+Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
+Proof.
+intros n m; unfold NZplus, NZsucc, NZE. rewrite w_spec.(spec_add).
+do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add).
+rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
+rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l; [ |apply gt_wB_0].
+rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc.
+Qed.
+
+Theorem NZminus_0_r : forall n : NZ, n - 0 == n.
+Proof.
+intro n; unfold NZminus, NZ0, NZE. rewrite w_spec.(spec_sub).
+rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod.
+Qed.
+
+Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m).
+Proof.
+intros n m; unfold NZminus, NZsucc, NZpred, NZE.
+rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub).
+rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r; [ | apply gt_wB_0].
+rewrite Zminus_mod_idemp_l; [ | apply gt_wB_0].
+now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith.
+Qed.
+
+Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0.
+Proof.
+intro n; unfold NZtimes, NZ0, NZ, NZE. rewrite w_spec.(spec_mul).
+rewrite w_spec.(spec_0). now rewrite Zmult_0_r.
+Qed.
+
+Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
+Proof.
+intros n m; unfold NZtimes, NZsucc, NZplus, NZE. rewrite w_spec.(spec_mul).
+rewrite w_spec.(spec_add). rewrite w_spec.(spec_mul). rewrite w_spec.(spec_succ).
+rewrite Zplus_mod_idemp_l; [ | apply gt_wB_0]. rewrite Zmult_mod_idemp_r; [ | apply gt_wB_0].
+rewrite Zmult_plus_distr_r. now rewrite Zmult_1_r.
+Qed.
+
+End NZBigIntsAxiomsMod.