feat(algebra): define "Euclidean" absolute values
A euclidean absolute value `abv : euclidean_absolute_value R S` is an absolute value that agrees with the Euclidean domain structure on `R`, namely `abv x < abv y ↔ euclidean_domain.r x y`.
Examples include `abs : ℤ → ℤ` and `λ (p : polynomial Fq), (q ^ p.degree : ℤ)`, where `Fq` is a finite field with `q` elements.
