proposition: Theorem next_pos: forall p, pos2n (next p) = S (pos2n p).
proof: Proof. intros (x, y); simpl; auto. unfold pos2n. case (eq_nat (S y) size); simpl; intros H1. rewrite <- H1. destruct (eq_nat y y); try lia. destruct size. + lia. + assert (y <> n) by lia. destruct (eq_nat y n); try lia. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia