cases m with
| zero => rwa [evr.zero_valtn_decr h]
| succ m =>
  have x_pos_val : evr.valtn x > 0 := by
    rw [h]
    exact NeZero.pos _
  simp at * sorry
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
m : ℕ
x : R
h : v evr.valtn x = ↑m
⊢ v evr.valtn (decr_val evr x) = ↑m - 1
no goals