proposition: Lemma drop_concatenate {A: UU} (l1 l2: list A) (n: nat) (nok: n ≤ length l1): drop (l1 ++ l2) n = (drop l1 n) ++ l2.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe