Library probsa.util.iota

(* --------------------------- Reals and SSReflect -------------------------- *)
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype bigop.

(* ---------------------------------- Main ---------------------------------- *)

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 ].