exact factorization'.coprime_of_mem h hbmem
case hx
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
⊢ IsCoprime b.re b.im
no goals