have pos_val : evr.valtn (sub_val evr n x) > 0 := by
  have h' := val_sub_val_le evr x n h
  rw [Nat.succ_eq_add_one] at h'
  norm_cast at h'
  rw [Nat.add_sub_self_left] at h'
  exact one_le_iff_pos.mp h'
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
⊢ x = p ^ n * (p * decr_val evr (sub_val evr n x))
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
ih : ↑n ≤ v evr.valtn x → x = p ^ n * sub_val evr n x
h : ↑(Nat.succ n) ≤ v evr.valtn x
pos_val : v evr.valtn (sub_val evr n x) > 0
⊢ x = p ^ n * (p * decr_val evr (sub_val evr n x))