From 76ebc736158c97c23a47492bcda9f9daaedc7ed7 Mon Sep 17 00:00:00 2001
From: thery
Date: Fri, 16 Feb 2018 16:13:30 +0100
Subject: generalize nth_iota

---
 mathcomp/ssreflect/seq.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5574892..8969e62 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2227,7 +2227,7 @@ Qed.
 Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
 Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed.
 
-Lemma nth_iota m n i : i < n -> nth 0 (iota m n) i = m + i.
+Lemma nth_iota p m n i : i < n -> nth p (iota m n) i = m + i.
 Proof.
 by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn.
 Qed.
-- 
cgit v1.2.3