proposition: Theorem prod_prime_le : forall (c n : nat) (f : nat -> nat), power 2 4 <= n -> 0 < c -> (forall x : nat, x <= n -> prime x -> f x <= c) -> (forall x : nat, x <= n -> ~ prime x -> f x = 1) -> prod_nm 0 n (fun x => f x) <= power c (div n 2 - 1).
proof: Proof. intros c n f H H0 H1 H2. rewrite <- (Nat.sub_add (power 2 4) n); auto; apply prod_prime_le_aux; auto with arith. intros x; rewrite (Nat.sub_add (power 2 4) n); auto with arith. intros x; rewrite (Nat.sub_add (power 2 4) n); auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)