From d2d0b966db4b899ac46d57e6f39b5c3b8c5c3753 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Dec 2006 10:38:20 +0000
Subject: Bug nommage Zgt_trans_succ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9438 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zorder.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 4b0d2562e7..45369561d1 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -549,7 +549,7 @@ Hint Immediate Zeq_le: zarith.
 
 (** Transitivity using successor *)
 
-Lemma Zge_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
+Lemma Zgt_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
 Proof.
   intros n m p H1 H2; apply Zle_gt_trans with (m := m);
     [ apply Zgt_succ_le; assumption | assumption ].
-- 
cgit v1.2.3