proposition: Theorem prod_prime_lt : forall n : nat, 1 < n -> prod_nm 0 n (fun x => prime_dirac x) < power 4 n.
proof: Proof. intros n; pattern n in |- *; apply lt_wf_ind; clear n; intros n. case (odd_or_even n). intros (x, H2); rewrite H2. case x. intros Rec H1; inversion H1. intros x1; case x1. simpl in |- *; auto with arith. intros x2 Rec H1. cut (2 * S (S x2) = S (S x2 + S (S x2))); [ intros H3 | auto with arith ]. rewrite H3; rewrite prod_nm_f. replace (prime_dirac (0 + S (S x2 + S (S x2)))) with 1. rewrite Nat.mul_1_r; auto. apply Nat.lt_trans with (power 4 (S x2 + S (S x2))); auto with arith. apply Rec; auto with arith. rewrite H3; auto with arith. rewrite <- plus_n_Sm; auto with arith. apply power_lt_mono; auto with arith. simpl in |- *; unfold prime_dirac in |- *. generalize (primeb_correct (S (S (x2 + S (S x2))))); case (primeb (S (S (x2 + S (S x2))))); auto. intros (H4, H5); absurd (S (S (x2 + S (S x2))) = 2); auto with arith. rewrite <- plus_n_Sm; red in |- *; intros H6; discriminate. apply H5; auto. exists (S (S x2)); auto with arith. rewrite Nat.mul_comm; rewrite H3; auto with arith. simpl in |- *; repeat rewrite <- plus_n_Sm; rewrite <- plus_n_O; auto with arith. intros (x1, H1); rewrite H1; intros Rec H2. cut (1 <= x1); [ intros Hx1 | generalize H2; case x1; simpl in |- *; auto with arith ]. rewrite prod_nm_split with (r := x1 + 1); auto with arith. 2: replace (x1 + 1) with (x1 + 1 + 0); auto with arith; replace (2 * x1 + 1) with (x1 + 1 + x1); auto with arith; ring. apply Nat.le_lt_trans with (prod_nm 0 (x1 + 1) (fun x : nat => prime_dirac x) * binomial (2 * x1 + 1) (x1 + 1)). apply (fun m n p : nat => Nat.mul_le_mono_l p n m). apply divides_le; auto with arith. apply Nat.neq_0_lt_0; auto with arith. replace (2 * x1 + 1) with (x1 + 1 + x1); auto with arith. apply binomial_lt; auto with arith. simpl in |- *; ring. replace (1 + (0 + (x1 + 1))) with (x1 + 2); [ idtac | ring ]. replace (2 * x1 + 1 - (1 + (x1 + 1))) with (x1 - 1); [ idtac | idtac ]. apply prod_prime_dirac_div. intros x H H0. replace (2 * x1 + 1) with (x1 + 1 + x1); [ idtac | ring ]. apply prime_dirac_divides_binomial; auto with arith. apply Nat.lt_le_trans with (2 := H); auto with arith. apply Nat.lt_le_trans with (2 := H); auto with arith. rewrite Nat.add_comm; auto with arith. replace (x1 + 1 + x1) with (x1 + 2 + (x1 - 1)); auto. pattern x1 at 4 in |- *; (rewrite <- Nat.sub_add with (n := 1); [ ring | auto ]). apply eq_sym. apply Nat.add_sub_eq_l. repeat rewrite <- Nat.add_assoc. rewrite <- (Nat.add_comm (x1 - 1)). simpl. rewrite Nat.sub_add; [ ring | auto ]. apply Nat.le_lt_trans with (prod_nm 0 (x1 + 1) (fun x : nat => prime_dirac x) * power 2 (2 * x1)). apply (fun m n p : nat => Nat.mul_le_mono_l p n m). apply binomial_odd. replace (power 4 (2 * x1 + 1)) with (power 4 (x1 + 1) * power 2 (2 * x1)). repeat rewrite (fun x y => Nat.mul_comm x (power 2 y)). apply mult_lt_bis; auto with arith. apply power_lt_O; auto with arith. apply Rec; auto with arith. replace (x1 + 1) with (x1 + 1 + 0); auto with arith; replace (2 * x1 + 1) with (x1 + 1 + x1); auto with arith; ring. change (0 + 1 < x1 + 1) in |- *; auto with arith. rewrite <- power_power. simpl in |- *; rewrite power_mult. repeat rewrite <- plus_n_Sm; repeat rewrite <- plus_n_O; auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)