proposition: Fact nthprime_nxt i p q : nthprime i = p -> nxtprime p = q -> nthprime (S i) = q.
proof: Proof. replace (S i) with (i+1) by lia. unfold nthprime at 2. rewrite iter_plus; fold (nthprime i). intros -> ?; simpl; 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)