proposition: Theorem prod_power_div_aux : forall n p q : nat, 0 < n -> p <= q -> (forall x : nat, p < 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 Hn H H0; case (proj1 (Nat.lt_eq_cases _ _) H); intros H1; [ idtac | rewrite H1 ]; auto. rewrite prod_nm_split with (r := p) (q := q); auto. replace (prod_nm (1 + (0 + p)) (q - (1 + p)) (fun x : nat => power (prime_dirac x) (power_div n x))) with 1; auto with arith. pattern 1 at 1 in |- *; rewrite <- (SO_power (S (q - (1 + p)))); apply sym_equal. rewrite <- prod_nm_c with (p := 1 + (0 + p)) (c := 1). apply prod_nm_ext. intros x H2. unfold prime_dirac in |- *; generalize (primeb_correct (1 + (0 + p) + x)); case (primeb (1 + (0 + p) + x)). intros H3; generalize (power_div_divides n (1 + (0 + p) + x)). case (power_div n (1 + (0 + p) + x)); auto. intros n0 H4; case (H0 (1 + (0 + p) + x)); auto with arith. rewrite <- (power_SO (1 + (0 + p) + x)); auto with arith. apply divides_trans with (power (1 + (0 + p) + x) (S n0)); auto with arith. apply H4; auto with arith. case (prime_2_or_more _ H3); auto with arith. intros H5; rewrite H5; auto with arith. intros H3; apply SO_power; auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)