proposition: Lemma nthprime_inj n m : nthprime n = nthprime m -> n = m.
proof: Proof. destruct (lt_eq_lt_dec n m) as [ [ H | ] | H ]; auto; intros; eapply nthprime_ge in H; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)