Implement Euclidean function for Euclidean domains #36
Description
It makes sense to require that all Euclidean domains provide a Euclidean function (though I'm not sure what to do when there is more than one).
It's not immediately clear if this can be done generically, for example, given a Euclidean division function one can't easily retrieve the Euclidean function. And given a Euclidean function, it is obviously possible to compute a GCD, but this might not even be the most efficient generic way of doing it, which raises the question: how does the implementation decide whether to use the Euclidean function or use the gcd function which is currently implemented in terms of the required Euclidean division function.
So the metaphysical question here is whether a Euclidean domain on a computer is a domain that provides a Euclidean division function, or whether it is a domain that provides a Euclidean function.