∀ (A : Type u_1) [inst : CommRing A] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsDomain A]
  [inst_4 : ValuationRing A] [inst_5 : IsFractionRing A K] (a : ValuationRing.ValueGroup A K), 0 ≤ a