EuclideanDomain instance for ℤ√(-2) (Zsqrtd (-2)) in ~60 lines, integer-only rounding

Mathlib v4.35 has the EuclideanDomain instance only for GaussianInt, and that one rounds through ℂ. For ℤ√(-2) you can stay in ℤ. Define rd a n := (2*a + n) / (2*n) (Int ediv). Then rd_spec: 0 < n → 4*(a - n*rd a n)^2 ≤ n^2. Prove it with Int.emod_add_mul_ediv, Int.emod_nonneg and Int.emod_lt_of_pos, then 2(a - nq) = r - n and nlinarith. Set x / y := ⟨rd (x*star y).re y.norm, rd (x*star y).im y.norm⟩ and x % y := x - y*(x/y). Key step: (x % y) * star y = ⟨A, B⟩ with A = c.re - n*rd c.re n (and B likewise), using y * star y = ↑y.norm (norm_eq_mul_conj). So N(r)*N(y) = A² + 2B² ≤ 3N(y)²/4, then lt_of_mul_lt_mul_right. Gotcha: set n := y.norm breaks the div_def rewrite (the unfolded div still shows y.norm while the goal has n). Introduce A and B with obtain ⟨A, hA⟩ : ∃ A, A = … := ⟨_, rfl⟩ instead. Instance fields as in GaussianInt: r_wellFounded := (measure (Int.natAbs ∘ norm)).wf, quotient_zero by ext <;> simp [div_def, rd] (Int division by 0 is 0). Name the instances explicitly, because the auto names contain _club and fail the defsWithUnderscore lint. After that, exists_associated_pow_of_mul_eq_pow' works out of the box, and x²+2=y³ is about 50 more lines.