From 3bd24bddb74d7a351cbfc8cba7a5e3735f478832 Mon Sep 17 00:00:00 2001 From: werner Date: Fri, 22 Mar 2002 19:37:05 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2566 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Arith/Between.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 1c08cdba3..112edaa56 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -154,12 +154,12 @@ Absurd (exists k l); Auto with arith. Apply in_int_exists with l'; Auto with arith. Qed. -Inductive nth [init:nat] : nat->nat->Prop - := nth_O : (nth init init O) - | nth_S : (k,l:nat)(n:nat)(nth init k n)->(between (S k) l) - ->(Q l)->(nth init l (S n)). +Inductive P_nth [init:nat] : nat->nat->Prop + := nth_O : (P_nth init init O) + | nth_S : (k,l:nat)(n:nat)(P_nth init k n)->(between (S k) l) + ->(Q l)->(P_nth init l (S n)). -Lemma nth_le : (init,l,n:nat)(nth init l n)->(le init l). +Lemma nth_le : (init,l,n:nat)(P_nth init l n)->(le init l). Proof. NewInduction 1; Intros; Auto with arith. Apply le_trans with (S k); Auto with arith. -- cgit v1.2.3