summaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer/NatPairs
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /theories/Numbers/Integer/NatPairs
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/Numbers/Integer/NatPairs')
-rw-r--r--theories/Numbers/Integer/NatPairs/ZNatPairs.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 8b3d815d..9427b37b 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: ZNatPairs.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: ZNatPairs.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Import NSub. (* The most complete file for natural numbers *)
Require Export ZMulOrder. (* The most complete file for integers *)
@@ -110,7 +110,7 @@ Proof.
unfold reflexive, Zeq. reflexivity.
Qed.
-Theorem ZE_symm : symmetric Z Zeq.
+Theorem ZE_sym : symmetric Z Zeq.
Proof.
unfold symmetric, Zeq; now symmetry.
Qed.
@@ -127,7 +127,7 @@ Qed.
Theorem NZeq_equiv : equiv Z Zeq.
Proof.
-unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
+unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_sym].
Qed.
Add Relation Z Zeq