proposition: Lemma map_nth_iota s i j : j <= size s - i -> [seq nth x0 s k | k <- iota i j] = take j (drop i s).
proof: Proof. elim: i => [|i IH] in s j *; first by rewrite subn0 drop0 => /map_nth_iota0->. case: s => [|x s /IH<-]; first by rewrite leqn0 => /eqP->. by rewrite -add1n iotaDl -map_comp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)