proposition: Theorem prod_prime_dirac_div : forall n m p : nat, (forall x : nat, n <= x -> x <= n + m -> divides (prime_dirac x) p) -> divides (prod_nm n m (fun x => prime_dirac x)) p.
proof: Proof. intros n m; elim m; auto. simpl in |- *; auto with arith. intros m1 H p H0. rewrite prod_nm_f. cut (divides (prime_dirac (n + S m1)) p); auto with arith. unfold prime_dirac in |- *; generalize (primeb_correct (n + S m1)); case (primeb (n + S m1)); fold prime_dirac in |- *; intros H1 (x, H2); rewrite H2. apply divides_mult; auto with arith. apply H; auto with arith. intros x1 H3 H4. cut (divides (prime_dirac x1) p); auto with arith. unfold prime_dirac in |- *; generalize (primeb_correct x1); case (primeb x1); fold prime_dirac in |- *; intros H5 H6. apply L_Euclides1 with (a := n + S m1); auto with arith. rewrite Nat.mul_comm; rewrite <- H2; auto. red in |- *; intros H7; absurd (x1 = n + S m1). red in |- *; intros H8; Contradict H4; auto. rewrite H8; auto with arith. case H1; intros H8 H9; apply sym_equal; apply H9; auto with arith. red in |- *; intros H10; Contradict H5; auto; rewrite H10; auto with arith. apply SO_divides_all. apply H0; auto with arith. apply Nat.le_trans with (1 := H4); auto with arith. repeat rewrite Nat.mul_1_r. apply H; auto with arith. intros x1 H3 H4. rewrite Nat.mul_1_r in H2; rewrite <- H2; auto with arith. apply H0; auto with arith. apply Nat.le_trans with (1 := H4); auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)