proposition: Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i.
proof: Proof. move=> lt_i_n0 s; case lt_n0_s: (n0 < size s). by rewrite -[s in RHS]cat_take_drop nth_cat size_take lt_n0_s /= lt_i_n0. by rewrite -[s in LHS]cats0 take_cat lt_n0_s /= cats0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)