fact: Fixpoint notprime_bool_rec n k := match k with | 0 => true | S k' => negb (prime_bool n) && notprime_bool_rec (S n) k' end.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)