proposition: Theorem prime_dirac_le_1 : forall n : nat, 1 <= prime_dirac n.
proof: Proof. intros n; generalize (prime_2_or_more n); unfold prime_dirac in |- *; generalize (primeb_correct n); case (primeb n); auto with arith. intros H1 H2; case (H2 H1); auto with arith; intros H3; rewrite H3 || apply Nat.lt_le_incl; auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)