proposition: Theorem prod_prime_dirac_le_1 : forall n : nat, 1 <= prod_nm 0 n (fun x => prime_dirac x).
proof: Proof. intros n; elim n; auto. intros n0 H; rewrite prod_nm_f. apply Nat.le_trans with (prod_nm 0 n0 (fun x : nat => prime_dirac x) * 1); auto with arith. apply (fun m n p : nat => Nat.mul_le_mono_l p n m). apply prime_dirac_le_1. Qed.
imports: Coq(ArithRing Wf_nat Lia)