∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {abv : AbsoluteValue R S} {x y : R}, abv.IsEuclidean → (abv x < abv y) = EuclideanDomain.r x y