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