Lemma length_drop {A: UU} (l: list A) (n: nat): length (drop l n) = length l - n. Proof. revert l n. refine (list_ind _ _ _). - intro n. rewrite drop_nil. induction n. + apply idpath. + change (0 = 0 - (1+ n)). rewrite <- natminusminus. assumption. - intros x xs IH. induction n. + apply idpath. + rewrite drop_step. rewrite length_cons. apply (IH n). Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.