rwa [evr.zero_valtn_decr h]
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = ↑Nat.zero
⊢ v evr.valtn (decr_val evr x) = ↑Nat.zero - 1
no goals