From 1e57f0c3312713ac6137da0c3612605501f65d58 Mon Sep 17 00:00:00 2001
From: emakarov
Date: Wed, 7 Nov 2007 18:39:28 +0000
Subject: Replaced BinNat with a new version that is based on
 theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new
 BinNat are notations for the development in Numbers. Also added min and max
 to the new natural numbers and integers.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/TreeMod/ZTreeMod.v | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

(limited to 'theories/Numbers/Integer/TreeMod')

diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index 7ee894ca4c..75e9c9f77e 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NZAxioms.
 Require Import NMake. (* contains W0Type *)
 Require Import ZnZ.
@@ -24,17 +36,17 @@ Definition NZplus := w_op.(znz_add).
 Definition NZminus := w_op.(znz_sub).
 Definition NZtimes := w_op.(znz_mul).
 
-Theorem NZE_equiv : equiv NZ NZeq.
+Theorem NZeq_equiv : equiv NZ NZeq.
 Proof.
 unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto.
 now transitivity [| y |].
 Qed.
 
 Add Relation NZ NZeq
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+as NZeq_rel.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
-- 
cgit v1.2.3