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 : Zsqrtd.norm b = Zsqrtd.norm c
⊢ OddPrimeOrFour (Zsqrtd.norm b)
no goals