13 files changed, 579 insertions, 0 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
new file mode 100644
index 000000000..4019b4774
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -0,0 +1,160 @@
+Require Export NumPrelude.
+Require Export NZAxioms.
+
+Set Implicit Arguments.
+
+Module Type ZAxiomsSig.
+
+Parameter Inline Z : Set.
+Parameter Inline ZE : Z -> Z -> Prop.
+Parameter Inline Z0 : Z.
+Parameter Inline Zsucc : Z -> Z.
+Parameter Inline Zpred : Z -> Z.
+Parameter Inline Zplus : Z -> Z -> Z.
+Parameter Inline Zminus : Z -> Z -> Z.
+Parameter Inline Ztimes : Z -> Z -> Z.
+Parameter Inline Zlt : Z -> Z -> Prop.
+Parameter Inline Zle : Z -> Z -> Prop.
+
+Delimit Scope IntScope with Int.
+Open Local Scope IntScope.
+Notation "x == y" := (ZE x y) (at level 70, no associativity) : IntScope.
+Notation "x ~= y" := (~ ZE x y) (at level 70, no associativity) : IntScope.
+Notation "0" := Z0 : IntScope.
+Notation "'S'" := Zsucc : IntScope.
+Notation "'P'" := Zpred : IntScope.
+Notation "1" := (S 0) : IntScope.
+Notation "x + y" := (Zplus x y) : IntScope.
+Notation "x - y" := (Zminus x y) : IntScope.
+Notation "x * y" := (Ztimes x y) : IntScope.
+Notation "x < y" := (Zlt x y) : IntScope.
+Notation "x <= y" := (Zle x y) : IntScope.
+Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
+Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
+
+Axiom ZE_equiv : equiv Z ZE.
+
+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.
+
+Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
+Add Morphism Zpred with signature ZE ==> ZE as Zpred_wd.
+Add Morphism Zplus with signature ZE ==> ZE ==> ZE as Zplus_wd.
+Add Morphism Zminus with signature ZE ==> ZE ==> ZE as Zminus_wd.
+Add Morphism Ztimes with signature ZE ==> ZE ==> ZE as Ztimes_wd.
+Add Morphism Zlt with signature ZE ==> ZE ==> iff as Zlt_wd.
+Add Morphism Zle with signature ZE ==> ZE ==> iff as Zle_wd.
+
+Axiom S_inj : forall x y : Z, S x == S y -> x == y.
+Axiom S_P : forall x : Z, S (P x) == x.
+
+Axiom induction :
+  forall Q : Z -> Prop,
+    pred_wd E Q -> Q 0 ->
+    (forall x, Q x -> Q (S x)) ->
+    (forall x, Q x -> Q (P x)) -> forall x, Q x.
+
+End IntSignature.
+
+Module IntProperties (Import IntModule : IntSignature).
+Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule.
+Open Local Scope IntScope.
+
+Ltac induct n :=
+  try intros until n;
+  pattern n; apply induction; clear n;
+  [unfold NumPrelude.pred_wd;
+  let n := fresh "n" in
+  let m := fresh "m" in
+  let H := fresh "H" in intros n m H; qmorphism n m | | |].
+
+Theorem P_inj : forall x y, P x == P y -> x == y.
+Proof.
+intros x y H.
+setoid_replace x with (S (P x)); [| symmetry; apply S_P].
+setoid_replace y with (S (P y)); [| symmetry; apply S_P].
+now rewrite H.
+Qed.
+
+Theorem P_S : forall x, P (S x) == x.
+Proof.
+intro x.
+apply S_inj.
+now rewrite S_P.
+Qed.
+
+(* The following tactics are intended for replacing a certain
+occurrence of a term t in the goal by (S (P t)) or by (P (S t)).
+Unfortunately, this cannot be done by setoid_replace tactic for two
+reasons. First, it seems impossible to do rewriting when one side of
+the equation in question (S_P or P_S) is a variable, due to bug 1604.
+This does not work even when the predicate is an identifier (e.g.,
+when one tries to rewrite (Q x) into (Q (S (P x)))). Second, the
+setoid_rewrite tactic, like the ordinary rewrite tactic, does not
+allow specifying the exact occurrence of the term to be rewritten. Now
+while not in the setoid context, this occurrence can be specified
+using the pattern tactic, it does not work with setoids, since pattern
+creates a lambda abstractuion, and setoid_rewrite does not work with
+them. *)
+
+Ltac rewrite_SP t set_tac repl thm :=
+let x := fresh "x" in
+set_tac x t;
+setoid_replace x with (repl x); [| symmetry; apply thm];
+unfold x; clear x.
+
+Tactic Notation "rewrite_S_P" constr(t) :=
+rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) S_P.
+
+Tactic Notation "rewrite_S_P" constr(t) "at" integer(k) :=
+rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) S_P.
+
+Tactic Notation "rewrite_P_S" constr(t) :=
+rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) P_S.
+
+Tactic Notation "rewrite_P_S" constr(t) "at" integer(k) :=
+rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) P_S.
+
+(* One can add tactic notations for replacements in assumptions rather
+than in the goal. For the reason of many possible variants, the core
+of the tactic is factored out. *)
+
+Section Induction.
+
+Variable Q : Z -> Prop.
+Hypothesis Q_wd : pred_wd E Q.
+
+Add Morphism Q with signature E ==> iff as Q_morph.
+Proof Q_wd.
+
+Theorem induction_n :
+  forall n, Q n ->
+    (forall m, Q m -> Q (S m)) ->
+    (forall m, Q m -> Q (P m)) -> forall m, Q m.
+Proof.
+induct n.
+intros; now apply induction.
+intros n IH H1 H2 H3; apply IH; try assumption. apply H3 in H1; now rewrite P_S in H1.
+intros n IH H1 H2 H3; apply IH; try assumption. apply H2 in H1; now rewrite S_P in H1.
+Qed.
+
+End Induction.
+
+Ltac induct_n k n :=
+  try intros until k;
+  pattern k; apply induction_n with (n := n); clear k;
+  [unfold NumPrelude.pred_wd;
+  let n := fresh "n" in
+  let m := fresh "m" in
+  let H := fresh "H" in intros n m H; qmorphism n m | | |].
+
+End IntProperties.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Axioms/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index e0b753d4e..e0b753d4e 100644
--- a/theories/Numbers/Integer/Axioms/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
diff --git a/theories/Numbers/Integer/Axioms/ZDec.v b/theories/Numbers/Integer/Abstract/ZDec.v
index 9a7aaa099..9a7aaa099 100644
--- a/theories/Numbers/Integer/Axioms/ZDec.v
+++ b/theories/Numbers/Integer/Abstract/ZDec.v
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 028128cf7..028128cf7 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index cc834b442..cc834b442 100644
--- a/theories/Numbers/Integer/Axioms/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index 624f85f04..624f85f04 100644
--- a/theories/Numbers/Integer/Axioms/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 95f0fa8c6..95f0fa8c6 100644
--- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
diff --git a/theories/Numbers/Integer/Axioms/ZPred.v b/theories/Numbers/Integer/Abstract/ZPred.v
index ffcb2dea8..ffcb2dea8 100644
--- a/theories/Numbers/Integer/Axioms/ZPred.v
+++ b/theories/Numbers/Integer/Abstract/ZPred.v
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 38311aa2b..38311aa2b 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index 055342bcc..055342bcc 100644
--- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
diff --git a/theories/Numbers/Integer/BigInts/EZBase.v b/theories/Numbers/Integer/BigInts/EZBase.v
new file mode 100644
index 000000000..f5c19c611
--- /dev/null
+++ b/theories/Numbers/Integer/BigInts/EZBase.v
@@ -0,0 +1,167 @@
+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.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v
new file mode 100644
index 000000000..ca3286211
--- /dev/null
+++ b/theories/Numbers/Integer/BigInts/Zeqmod.v
@@ -0,0 +1,48 @@
+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.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
new file mode 100644
index 000000000..217d08850
--- /dev/null
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -0,0 +1,204 @@
+Require Import ZTimesOrder.
+Require Import ZArith.
+
+Open Local Scope Z_scope.
+Module Export ZBinDomain <: ZDomainSignature.
+Delimit Scope IntScope with Int.
+(* Is this really necessary? Without it, applying ZDomainProperties
+functor to this module produces an error since the functor opens the
+scope. *)
+
+Definition Z := Z.
+Definition E := (@eq Z).
+Definition e := Zeq_bool.
+
+Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
+Proof.
+intros x y; unfold E, e, Zeq_bool; split; intro H.
+rewrite H; now rewrite Zcompare_refl.
+rewrite eq_true_unfold_pos in H.
+assert (H1 : (x ?= y) = Eq).
+case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H;
+[reflexivity | discriminate H | discriminate H].
+now apply Zcompare_Eq_eq.
+Qed.
+
+Theorem E_equiv : equiv Z E.
+Proof.
+apply eq_equiv with (A := Z). (* It does not work without "with (A := Z)" though it looks like it should *)
+Qed.
+
+Add Relation Z E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+End ZBinDomain.
+
+Module Export ZBinInt <: IntSignature.
+Module Export ZDomainModule := ZBinDomain.
+
+Definition O := 0.
+Definition S := Zsucc'.
+Definition P := Zpred'.
+
+Add Morphism S with signature E ==> E as S_wd.
+Proof.
+intros; unfold E; congruence.
+Qed.
+
+Add Morphism P with signature E ==> E as P_wd.
+Proof.
+intros; unfold E; congruence.
+Qed.
+
+Theorem S_inj : forall x y : Z, S x = S y -> x = y.
+Proof.
+exact Zsucc'_inj.
+Qed.
+
+Theorem S_P : forall x : Z, S (P x) = x.
+Proof.
+exact Zsucc'_pred'.
+Qed.
+
+Theorem induction :
+  forall Q : Z -> Prop,
+    pred_wd E Q -> Q 0 ->
+    (forall x, Q x -> Q (S x)) ->
+    (forall x, Q x -> Q (P x)) -> forall x, Q x.
+Proof.
+intros; now apply Zind.
+Qed.
+
+End ZBinInt.
+
+Module Export ZBinPlus <: ZPlusSignature.
+Module Export IntModule := ZBinInt.
+
+Definition plus := Zplus.
+Definition minus := Zminus.
+Definition uminus := Zopp.
+
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+intros; congruence.
+Qed.
+
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Proof.
+intros; congruence.
+Qed.
+
+Add Morphism uminus with signature E ==> E as uminus_wd.
+Proof.
+intros; congruence.
+Qed.
+
+Theorem plus_0 : forall n, 0 + n = n.
+Proof.
+exact Zplus_0_l.
+Qed.
+
+Theorem plus_S : forall n m, (S n) + m = S (n + m).
+Proof.
+intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l.
+Qed.
+
+Theorem minus_0 : forall n, n - 0 = n.
+Proof.
+exact Zminus_0_r.
+Qed.
+
+Theorem minus_S : forall n m, n - (S m) = P (n - m).
+Proof.
+intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
+apply Zminus_succ_r.
+Qed.
+
+Theorem uminus_0 : - 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem uminus_S : forall n, - (S n) = P (- n).
+Admitted.
+
+End ZBinPlus.
+
+Module Export ZBinTimes <: ZTimesSignature.
+Module Export ZPlusModule := ZBinPlus.
+
+Definition times := Zmult.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem times_0 : forall n, n * 0 = 0.
+Proof.
+exact Zmult_0_r.
+Qed.
+
+Theorem times_S : forall n m, n * (S m) = n * m + n.
+Proof.
+intros; rewrite <- Zsucc_succ'; apply Zmult_succ_r.
+Qed.
+
+End ZBinTimes.
+
+Module Export ZBinOrder <: ZOrderSignature.
+Module Export IntModule := ZBinInt.
+
+Definition lt := Zlt_bool.
+Definition le := Zle_bool.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+congruence.
+Qed.
+
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+congruence.
+Qed.
+
+Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m.
+Proof.
+intros; unfold lt, le, Zlt_bool, Zle_bool.
+case_eq (n ?= m); intro H.
+apply Zcompare_Eq_eq in H; rewrite H; now split; intro; [right |].
+now split; intro; [left |].
+split; intro H1. now idtac.
+destruct H1 as [H1 | H1].
+assumption. unfold E in H1; rewrite H1 in H. now rewrite Zcompare_refl in H.
+Qed.
+
+Theorem lt_irr : forall n, ~ (lt n n).
+Proof.
+intro n; rewrite eq_true_unfold_pos; intro H.
+assert (H1 : (Zlt n n)).
+change (if true then (Zlt n n) else (Zge n n)). rewrite <- H.
+unfold lt. apply Zlt_cases.
+false_hyp H1 Zlt_irrefl.
+Qed.
+
+Theorem lt_S : forall n m, lt n (S m) <-> le n m.
+Proof.
+intros; unfold lt, le, S; do 2 rewrite eq_true_unfold_pos.
+rewrite <- Zsucc_succ'; rewrite <- Zlt_is_lt_bool; rewrite <- Zle_is_le_bool.
+split; intro; [now apply Zlt_succ_le | now apply Zle_lt_succ].
+Qed.
+
+End ZBinOrder.
+
+Module Export ZTimesOrderPropertiesModule :=
+  ZTimesOrderProperties ZBinTimes ZBinOrder.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)