proposition: Fact nxtprime_spec2 n : prime (nxtprime n).
proof: Proof. apply (proj2_sig (first_prime_above n)). Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)