Fundamental theorem of arithmetic (existence)

import Mathlib

theorem prime_factorization_exists (n : Nat) (h : 1 < n) : ∃ l : List Nat, (∀ p ∈ l, Nat.Prime p) ∧ l.prod = n :=by
  use n.primeFactorsList
  refine ⟨fun p hp => Nat.prime_of_mem_primeFactorsList hp, ?_⟩
  exact Nat.prod_primeFactorsList (by omega)