proposition: Theorem get_next: forall p a s, get (next p) (a :: s) = get p s.
proof: Proof. intros p a s. induction p. - simpl. destruct (eq_nat (S n0) size). + rewrite <- !e. destruct (eq_nat n0 n0); try lia. unfold get. simpl. rewrite <- !e. simpl. f_equal. f_equal. lia. + case_eq size. * intros. unfold get. simpl. rewrite <- plus_n_Sm. simpl. reflexivity. * intros. destruct (eq_nat n0 n2); try lia. unfold get. simpl. rewrite <- plus_n_Sm. simpl. reflexivity. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia