proposition: Theorem factorization : forall n p : nat, 0 < n -> (forall x : nat, p < x -> prime x -> ~ divides x n) -> n = prod_nm 0 p (fun x : nat => power (prime_dirac x) (power_div n x)).
proof: Proof. intros n; pattern n in |- *; apply lt_wf_ind; clear n. intros n H p H0 H1. cut (forall p : nat, 0 < p -> forall x : nat, p < x -> prime x -> ~ divides x p); [ intros Hp | idtac ]. generalize (max_div_prop1 n); generalize (max_div_prop2 n); generalize (max_div_prop3 n); case (max_div n). intros H2 H3 (x, H4); Contradict H0; auto; rewrite H4; rewrite <- mult_n_O; auto with arith. intros m1; case m1. intros H2 H3 H4. 2: intros n0 H2 H3 (x, H4); rewrite H4. 2: cut (0 < x); [ intros Hx | generalize H0; rewrite H4; case x; simpl in |- *; auto with arith ]. 2: pattern x at 1 in |- *; rewrite H with (m := x) (p := x); auto with arith. 2: pattern (S (S n0)) at 1 in |- *; rewrite H with (m := S (S n0)) (p := S (S n0)); auto with arith. 2: apply sym_equal; apply prod_power_div_mult; auto with arith. 2: rewrite <- H4; auto. 2: apply H2; rewrite H4; inversion Hx; simpl in |- *; auto with arith. 2: rewrite H4; rewrite Nat.mul_comm; inversion Hx; simpl in |- *; try rewrite <- plus_n_Sm; auto with arith. 2: intros p0 H2 x H3 H4; red in |- *; intros H5; Contradict H3; auto with arith. 2: apply Nat.le_ngt; apply divides_le; auto with arith. 2: apply sym_not_equal; auto with arith. cut (prime n \/ n = 1); [ intros H5; case H5; intros H6 | idtac ]. rewrite prod_power_div with (q := n); auto with arith. pattern n at 2 in |- *; rewrite <- (Nat.lt_succ_pred 0 n); auto with arith. rewrite prod_nm_f; auto with arith. rewrite (Nat.lt_succ_pred 0 n); auto with arith. replace (prod_nm 0 (pred n) (fun x : nat => power (prime_dirac x) (power_div n x))) with (power 1 (S (pred n))). rewrite SO_power; simpl in |- *; rewrite <- plus_n_O. rewrite prime_prime_dirac; try rewrite power_div_id; simpl in |- *; auto with arith. rewrite <- prod_nm_c with (p := 0). apply prod_nm_ext. intros x H7; simpl in |- *. generalize (power_div_divides n x H0); generalize (H3 x); generalize H7. case x. rewrite not_prime_prime_dirac; try rewrite SO_power; auto with arith. intros x1; case x1. rewrite not_prime_prime_dirac; try rewrite SO_power; auto with arith. intros x2; case (power_div n (S (S x2))). simpl in |- *; auto. intros n0 H8 H9 H10; absurd (divides (S (S x2)) n); auto. apply H9; auto with arith. apply Nat.le_lt_trans with (1 := H8); auto with arith. rewrite <- (fun x => power_SO (S (S x))); apply divides_trans with (power (S (S x2)) (S n0)); auto with arith. rewrite prod_power_div with (q := 1); auto with arith. simpl in |- *; auto with arith. rewrite H6; repeat rewrite not_prime_prime_dirac; auto with arith. rewrite H6. intros x H7 H8; apply not_lt_div; auto with arith. generalize H3; inversion H0; auto. case m; auto. intros n0 H7; left; split; auto with arith. intros b H8 H9; apply Nat.le_antisymm. case (Nat.le_gt_cases (S (S n0)) b); auto; intros H10. case (H7 b); auto with arith. generalize H8 H9; case b; simpl in |- *; auto with arith. intros (x, H11); rewrite Nat.mul_comm in H11; discriminate. intros x; case x; auto with arith. intros H11 H12; case H12; auto. apply divides_le; auto. Qed.
imports: Coq(ArithRing Wf_nat Lia)