rw [mul_eq_zero] at v_decr_zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p * decr_val evr 0 = 0
⊢ decr_val evr 0 = 0
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
v_decr_zero : p = 0 ∨ decr_val evr 0 = 0
⊢ decr_val evr 0 = 0