theorem Zsqrtd.exists {d : ℤ} (a : ℤ√d) (him : a.im ≠ 0) : ∃ c, Zsqrtd.norm a = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

theorem factors2 {a : ℤ√(-3)} (heven : Even (Zsqrtd.norm a)) : ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

theorem Spts.mul_of_dvd' {a : ℤ√(-3)} {p : ℤ√(-3)} (hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a) (hpprime : Prime (Zsqrtd.norm p)) : ∃ u, a = p * u ∨ a = star p * u

theorem Spts.mul_of_dvd'' {a : ℤ√(-3)} {p : ℤ√(-3)} (hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a) (hpprime : Prime (Zsqrtd.norm p)) : ∃ u, (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u

theorem factors' (a : ℤ√(-3)) (f : ℤ) (g : ℤ) (hodd : Odd f) (hgpos : g ≠ 0) (hfactor : f * g = Zsqrtd.norm a) (hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = Zsqrtd.norm p) : ∃ p, |f| = Zsqrtd.norm p

theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) : ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2

theorem Zqrtd.factor_div' (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) (h : 1 < |x|) (hcoprime : IsCoprime a.re a.im) (hfactor : x ∣ Zsqrtd.norm a) : ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2 ∧ c ≠ 0 ∧ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x

theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hodd : Odd x) (hfactor : x ∣ Zsqrtd.norm a) : ∃ c, |x| = Zsqrtd.norm c

theorem Spts.eq_one {a : ℤ√(-3)} (h : Zsqrtd.norm a = 1) : |a.re| = 1 ∧ a.im = 0

theorem Spts.eq_one' {a : ℤ√(-3)} (h : Zsqrtd.norm a = 1) : a = 1 ∨ a = -1

theorem Spts.ne_zero_of_coprime' (a : ℤ√(-3)) (hcoprime : IsCoprime a.re a.im) : Zsqrtd.norm a ≠ 0

theorem Spts.pos_of_coprime' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : 0 < Zsqrtd.norm a

theorem Spts.one_lt_of_im_ne_zero (a : ℤ√(-3)) (hb : a.im ≠ 0) : 1 < Zsqrtd.norm a

theorem Spts.not_two (a : ℤ√(-3)) : Zsqrtd.norm a ≠ 2

theorem Spts.four {p : ℤ√(-3)} (hfour : Zsqrtd.norm p = 4) (hq : p.im ≠ 0) : |p.re| = 1 ∧ |p.im| = 1

theorem Spts.four_of_coprime {p : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hfour : Zsqrtd.norm p = 4) : |p.re| = 1 ∧ |p.im| = 1