apply associated'_of_associated_norm
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ Associated' b c
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
⊢ Associated b.norm c.norm

case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ IsCoprime b.re b.im

case hy
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ IsCoprime c.re c.im

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