proposition: Lemma nthprime_ge n m : n < m -> nthprime n < nthprime m.
proof: Proof. unfold nthprime. induction 1; simpl iter; rewrite iter_swap; auto. apply Nat.lt_trans with (2 := nxtprime_spec1 _); 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)