proposition: Lemma map_nth_iota0 s i : i <= size s -> [seq nth x0 s j | j <- iota 0 i] = take i s.
proof: Proof. by move=> ile; rewrite -[s in RHS]mkseq_nth -map_take take_iota (minn_idPl _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)