have v_decr_zero : p * evr.decr_val 0 = 0 := by
  symm
  apply evr.pos_valtn_decr
  rw [val_zero]
  decide
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ decr_val evr 0 = 0
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