proposition: Lemma primestream_divides (ps : primestream) n m : divides (ps n) (ps m) -> n = m.
proof: Proof. destruct ps as [ str H1 H2 ]; simpl. intros ? % prime_divides; eauto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)