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