diff options
Diffstat (limited to 'theories/Arith/Between.v')
| -rwxr-xr-x | theories/Arith/Between.v | 10 |
1 files 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. |