Lemma drop_concatenate {A: UU} (l1 l2: list A) (n: nat) (nok: n ≤ length l1): drop (l1 ++ l2) n = (drop l1 n) ++ l2. Proof. revert l1 nok. induction n. - reflexivity. - refine (list_ind _ _ _). + intros. contradiction (negnatlehsn0 _ nok). + intros x xs _ sok. rewrite concatenateStep. do 2rewrite drop_step. apply (IHn xs sok). Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.