proposition: Lemma nthprime_prime n : prime (nthprime n).
proof: Proof. unfold nthprime; destruct n; simpl; auto; rewrite iter_swap; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)