∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (r : R) (u : Rˣ)
  {ϖ : R}, Irreducible ϖ → ∀ (n : ℕ), r = ↑u * ϖ ^ n → (IsDiscreteValuationRing.addVal R) r = ↑n