rw [sub_val_val_pos_succ, sub_val_decr_val_comm, pow_succ', mul_assoc]
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 ^ Nat.succ n * sub_val evr (Nat.succ 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
⊢ x = p ^ n * (p * decr_val evr (sub_val evr n x))