fact: Record primestream := { str :> nat -> nat; str_inj : forall n m, str n = str m -> n = m; str_prime : forall n, prime (str n); }.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)