proposition: Theorem prod_prime_le_aux : forall (c n : nat) (f : nat -> nat), 0 < c -> (forall x : nat, x <= n + power 2 4 -> prime x -> f x <= c) -> (forall x : nat, x <= n + power 2 4 -> ~ prime x -> f x = 1) -> prod_nm 0 (n + power 2 4) (fun x => f x) <= power c (div (n + power 2 4) 2 - 1).
proof: Proof. intros c n. generalize (primeb_correct 0); intros P1; simpl in P1. generalize (primeb_correct 1); intros P2; simpl in P2. generalize (primeb_correct 2); intros P3; simpl in P3. generalize (primeb_correct 3); intros P4; simpl in P4. generalize (primeb_correct 4); intros P5; simpl in P5. generalize (primeb_correct 5); intros P6; simpl in P6. generalize (primeb_correct 6); intros P7; simpl in P7. generalize (primeb_correct 7); intros P8; simpl in P8. generalize (primeb_correct 8); intros P9; simpl in P9. generalize (primeb_correct 9); intros P10; simpl in P10. generalize (primeb_correct 10); intros P11; simpl in P11. generalize (primeb_correct 11); intros P12; simpl in P12. generalize (primeb_correct 12); intros P13; simpl in P13. generalize (primeb_correct 13); intros P14; simpl in P14. generalize (primeb_correct 14); intros P15; simpl in P15. generalize (primeb_correct 15); intros P16; simpl in P16. generalize (primeb_correct 16); intros P17; simpl in P17. generalize (primeb_correct 17); intros P18; simpl in P18. pattern n in |- *; apply lt_wf_ind; clear n. intros n; case n. simpl in |- *. intros Rec f H H0 H1. rewrite (H1 0); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 1); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 4); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 6); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 8); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 9); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 10); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 12); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 14); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 15); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 16); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. apply Nat.le_trans with (power c 6). simpl in |- *; repeat rewrite Nat.mul_1_r; repeat apply le_mult; auto; apply H0; repeat apply le_n_S; auto with arith. change (power c 6 <= power c 7) in |- *; apply power_le_mono; auto. clear n; intros n; case n. simpl in |- *. intros Rec f H H0 H1; try assumption. rewrite (H1 0); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 1); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 4); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 6); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 8); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 9); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 10); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 12); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 14); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 15); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. rewrite (H1 16); try rewrite Nat.mul_1_l; repeat apply le_n_S; auto with arith. simpl in |- *; repeat rewrite Nat.mul_1_r; repeat apply le_mult; auto; apply H0; repeat apply le_n_S; auto with arith. intros n0 Rec f H H0 H1. cut (1 <= div (n0 + power 2 4) 2); [ intros Hle | idtac ]. repeat (rewrite Nat.add_succ_comm; rewrite <- plus_n_Sm); repeat rewrite prod_nm_f. case (prime_dec (0 + S (n0 + power 2 4))); intros H4. rewrite (H1 (0 + S (S (n0 + power 2 4)))); auto with arith. rewrite Nat.mul_1_r. replace (div (S (S (n0 + power 2 4))) 2) with (div (2 + (n0 + power 2 4)) 2); [ rewrite div_plus | simpl in |- * ]; auto with arith. replace (power c (1 + div (n0 + power 2 4) 2 - 1)) with (power c (div (n0 + power 2 4) 2 - 1) * c). apply le_mult; auto with arith. apply Rec; auto with arith. intros x H5 H6; apply H0; auto with arith. apply Nat.le_trans with (1 := H5); auto with arith. intros x H5 H6; apply H1; auto with arith. apply Nat.le_trans with (1 := H5); auto with arith. pattern c at 2 in |- *; rewrite <- (power_SO c); rewrite power_mult. rewrite plus_minus_assoc; auto with arith. rewrite <- plus_n_Sm; auto with arith. apply prime_not_prime_S; auto with arith. simpl in |- *; rewrite <- plus_n_Sm; rewrite <- plus_n_Sm; auto with arith. rewrite H1; try rewrite Nat.mul_1_r; auto with arith. replace (div (S (S (n0 + power 2 4))) 2) with (div (2 + (n0 + power 2 4)) 2); [ rewrite div_plus | simpl in |- * ]; auto with arith. replace (power c (1 + div (n0 + power 2 4) 2 - 1)) with (power c (div (n0 + power 2 4) 2 - 1) * c). apply le_mult; auto with arith. apply Rec; auto with arith. intros x H5 H6; apply H0; auto with arith. apply Nat.le_trans with (1 := H5); auto with arith. intros x H5 H6; apply H1; auto with arith. apply Nat.le_trans with (1 := H5); auto with arith. case (prime_dec (0 + S (S (n0 + power 2 4)))); intros Hp'. simpl in |- *; auto with arith. rewrite H1; auto with arith. pattern c at 2 in |- *; rewrite <- (power_SO c); rewrite power_mult. rewrite plus_minus_assoc; auto with arith. simpl in |- *; replace (n0 + 16) with (2 + (n0 + 14)) by ring; rewrite div_plus; auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)