proposition: Theorem not_prime_prime_dirac : forall p : nat, ~ prime p -> prime_dirac p = 1.
proof: Proof. intros p; unfold prime_dirac in |- *; generalize (primeb_correct p); case (primeb p); auto with arith. intros H H0; case H0; auto. Qed.
imports: Coq(ArithRing Wf_nat Lia)