proposition: Fact prime_bool_rec_spec n p : n <= p -> prime_bool_rec n p = true <-> forall k, 3 <= n-2*k -> ~ n-2*k <d p.
proof: Proof. induction on n as IHn with measure n; intros Hn. destruct n as [ | [ | [ | n' ] ] ]. 1-3: split; try (simpl; auto; fail); intros _ k H; lia. unfold prime_bool_rec; fold (prime_bool_rec (S n') p). revert Hn; set (m := S n'); intros Hn. rewrite andb_true_iff, negb_true_iff, divides_bool_spec', IHn; try lia. split. + intros (H1 & H2) [ | q ] G1 G2. * apply H1 in G2; auto. * apply (H2 q); try lia. eq goal G2; f_equal; lia. + intros H1; split. * apply (H1 0); lia. * intros k G1 G2; apply (H1 (S k)); try lia. eq goal G2; f_equal; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)