proposition: Fact notprime_bool_rec_spec n k : notprime_bool_rec n k = true <-> forall i, n <= i < k+n -> ~ prime i.
proof: Proof. revert n; induction k as [ | k IHk ]; intros n; simpl. + split; auto; intros; lia. + rewrite andb_true_iff, negb_true_iff, <- not_true_iff_false, prime_bool_spec, IHk. split. * intros (H1 & H2) i Hi. destruct (eq_nat_dec n i); subst; auto. apply H2; lia. * intros H; split; intros; apply H; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)