proposition: Theorem prime_bool_spec' p : prime_bool p = false <-> ~ prime p.
proof: Proof. rewrite <- not_true_iff_false, prime_bool_spec; tauto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)