∀ {A : Type u_1} {B : Type u_2} {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : ValuativeRel A}
  {inst_3 : ValuativeRel B} {inst_4 : Algebra A B} [self : ValuativeExtension A B] (a b : A),
  (algebraMap A B) a ≤ᵥ (algebraMap A B) b ↔ a ≤ᵥ b