exact Or.resolve_left v_decr_zero (p_non_zero evr.valtn)
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
no goals