rw [evr.valtn.v_mul_eq_add_v, evr.valtn.v_uniformizer]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ v evr.valtn (p * x) > 0
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
⊢ 1 + v evr.valtn x > 0