proposition: Theorem length_update p v l : length (update p v l) = length l.
proof: Proof. unfold update; generalize v l; clear v l; elim (pos2n p); simpl; auto. intros v l; case l; auto. intros n1 Rec v l; case l; simpl; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia