proposition: Lemma ps_qs : forall n m, ps n = qs m -> False.
proof: Proof. intros ? ? ? % nthprime_inj; 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)