convert dvd_sub hfactor (dvd_mul_right x e)
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ x ∣ Zsqrtd.norm c
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ Zsqrtd.norm c = Zsqrtd.norm (c + m * ↑x) - x * e