Library probsa.util.iota
From
mathcomp
Require
Export
ssreflect
ssrnat
ssrbool
seq
eqtype
bigop
.
We prove that
[::
t1
;
t1
+1;
...;
t2
]
is equal to
[::
t1
;
t1
+1;
...;
t2
-1]
++
[::
t2
]
.
Lemma
index_iota_recr
:
∀
t1
t2
,
t1
≤
t2
→
index_iota
t1
t2
.+1
=
index_iota
t1
t2
++
[::
t2
]
.