summaryrefslogtreecommitdiff
path: root/theories/Numbers/NumPrelude.v
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/NumPrelude.v
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/Numbers/NumPrelude.v')
-rw-r--r--theories/Numbers/NumPrelude.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index fdccf214..95d8b366 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NumPrelude.v 10943 2008-05-19 08:45:13Z letouzey $ i*)
+(*i $Id: NumPrelude.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Export Setoid.
@@ -212,7 +212,7 @@ unfold reflexive, prod_rel.
destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
Qed.
-Lemma prod_rel_symm : symmetric (A * B) prod_rel.
+Lemma prod_rel_sym : symmetric (A * B) prod_rel.
Proof.
unfold symmetric, prod_rel.
destruct x; destruct y;
@@ -229,7 +229,7 @@ Qed.
Theorem prod_rel_equiv : equiv (A * B) prod_rel.
Proof.
-unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]].
+unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_sym]].
Qed.
End RelationOnProduct.