have hm : evr.valtn (-x) > 0 := by simp [h]
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
⊢ decr_val evr (-x) = -decr_val evr x
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
h : 0 < v evr.valtn x
hm : v evr.valtn (-x) > 0
⊢ decr_val evr (-x) = -decr_val evr x