exact ((factorization'_prop h).2 b hbmem).2.2
case h'
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ OddPrimeOrFour b.norm.natAbs
no goals