Lean4
/-- A noncomputable Euclidean domain structure on a discrete valuation ring, where the GCD algorithm
only takes two steps to terminate. Given `GCD(x,y)`, if `x ∣ y` then `y%x = 0` so we're done in one
step; otherwise `y%x = y` and then `GCD(x,y) = GCD(y,x)` which brings us back to the first case.
See `EuclideanDomain.to_principal_ideal_domain` for EuclideanDomain ⇒ PID. -/
def toEuclideanDomain : EuclideanDomain R where
quotient := quotient
quotient_zero x := by simp [quotient]
remainder := remainder
quotient_mul_add_remainder_eq x
y := by
rw [remainder, quotient]
split_ifs with h₁ h₂ h₂
· rw [h₁, zero_dvd_iff] at h₂; rw [h₁, h₂]; ring
· rw [h₁]; ring
· rw [← h₂.choose_spec]; ring
· ring
r x y := toWithBotNat x < toWithBotNat y
r_wellFounded := WellFounded.onFun wellFounded_lt
remainder_lt x y
hy := by
rw [remainder]
split_ifs with hyx
· rwa [toWithBotNat_zero, bot_lt_toWithBotNat_iff]
· exact lt_iff_not_ge.mpr (mt (dvd_of_toWithBotNat_le_toWithBotNat _ _ hy) hyx)
mul_left_not_lt x y
hy := by
by_cases hx : x = 0
· simp [hx]
rw [not_lt, toWithBotNat_le_toWithBotNat_iff hx (mul_ne_zero hx hy)]
exact dvd_mul_right _ _
