proposition: Lemma prime_qs n : prime (qs n).
proof: Proof. eapply nthprime_prime. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss) Undecidability.FRACTRAN(FRACTRAN_computable mm_fractran prime_seq) Undecidability.Shared.Libs.DLW(gcd prime vec) Nat Arith Lia List