proposition: Theorem prestrict_get s p q : pos2n p < pos2n q -> get p (prestrict q s) = get p s.
proof: Proof. intros H; unfold get, prestrict. repeat rewrite <- jump_nth; apply restrict_nth; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia