obtain ⟨h1, h2⟩ := factorization'_prop hcoprime
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
h1 : a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod
h2 : ∀ pq ∈ factorization' hcoprime, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g