proposition: Theorem prod_power_div : forall n p q : nat, 0 < n -> (forall x : nat, p < x -> prime x -> ~ divides x n) -> (forall x : nat, q < x -> prime x -> ~ divides x n) -> 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 n x)).
proof: Proof. intros n p q H H0 H1; case (Nat.le_gt_cases p q); intros H2. apply prod_power_div_aux; auto. apply sym_equal; apply prod_power_div_aux; auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)