proposition: Theorem prod_power_div_mult : forall n m p q r : nat, 0 < n -> 0 < m -> (forall x : nat, p < x -> prime x -> ~ divides x n) -> (forall x : nat, q < x -> prime x -> ~ divides x m) -> (forall x : nat, r < x -> prime x -> ~ divides x (n * m)) -> prod_nm 0 r (fun x : nat => power (prime_dirac x) (power_div (n * m) x)) = prod_nm 0 p (fun x : nat => power (prime_dirac x) (power_div n x)) * prod_nm 0 q (fun x : nat => power (prime_dirac x) (power_div m x)).
proof: Proof. intros n m p q r H H0 H1 H2 H3. rewrite prod_power_div with (p := p) (q := r); auto with arith. rewrite prod_power_div with (p := q) (q := r); auto with arith. rewrite prod_nm_mult; auto with arith. apply prod_nm_ext; auto with arith. intros x H4; simpl in |- *. unfold prime_dirac in |- *; generalize (primeb_correct x); case (primeb x). intros H5; rewrite power_div_mult_prime; auto with arith. apply sym_equal; apply power_mult. repeat rewrite SO_power; auto. intros x H4 H'4; red in |- *; intros H5; case (H3 x); auto with arith. apply divides_trans with (1 := H5); auto with arith. exists n; auto with arith. intros x H4 H'4; red in |- *; intros H5; case (H3 x); auto with arith. apply divides_trans with (1 := H5); auto with arith. exists m; auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)