proposition: Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
proof: Proof. rewrite -[s in RHS]cat_take_drop nth_cat size_take ltnNge. case: ltnP => [?|le_s_n0]; rewrite ?(leq_trans le_s_n0) ?leq_addr ?addKn //=. by rewrite drop_oversize // !nth_default. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)