HOL.Euclidean_Rings