proposition: Theorem update_get p v l : pos2n p < length l -> get p (update p v l) = v .
proof: Proof. unfold get, update; generalize (pos2n p); elim l; simpl; clear l p. intros n H; contradict H; auto with arith. intros a l1 Rec n; case n; clear n; simpl; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia