diff options
| author | Assia Mahboubi | 2018-03-06 14:38:04 +0100 |
|---|---|---|
| committer | GitHub | 2018-03-06 14:38:04 +0100 |
| commit | 3d59940ff4601713e8395f6b7e5c525501183731 (patch) | |
| tree | e472756b1d1d795e67b24e00c90d4ce3da099e2e /mathcomp | |
| parent | f26e353970e99ec25c540c92c9722ee4f578391b (diff) | |
| parent | 76ebc736158c97c23a47492bcda9f9daaedc7ed7 (diff) | |
Merge pull request #178 from thery/master
generalize the default value of nth in nth_iota
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index a562879..c1bf999 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. |