rw [evr.zero_valtn_decr h, evr.zero_valtn_decr hm]
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : v evr.valtn x = 0
hm : v evr.valtn (-x) = 0
⊢ decr_val evr (-x) = -decr_val evr x
no goals