theorem Nat.prod_primeFactors_factorization_apply (n : ℕ) {p : ℕ} (hp : Prime p) {f : ℕ → ℕ → ℕ} (hf : ∀ (q n : ℕ), ¬q ∣ n → f q n = 0) (hf₀ : ∀ (q : ℕ), f q 0 = 0) : (∏ q ∈ n.primeFactors, q ^ f q n).factorization p = f p n